Scaling Up Reasoning from Conditional Belief Bases
摘要
This paper introduces the online reasoning platform InfOCF-Web 2.0 that provides easy access to implementations of various inference methods for conditional belief bases. We present an overview of the realization of the inductive inference operator s p-entailment, system Z, c-inference, and system W. In order to address the fact that the possible worlds to be taken into account grow exponentially with the propositional signature over which the conditionals in the belief base are defined, the implementations employ SAT and Partial MaxSAT concepts and use the power of current SAT and SMT solvers. Our evaluation shows that each of the four inference operators can handle belief bases over signatures containing more than 100 variables and with more than 100 conditionals. Thus, InfOCF-Web 2.0 scales up nonmonotonic reasoning from conditionals to a new dimension because apart from the implementations now available in InfOCF-Web 2.0, there is no other implementation of an inference operator for conditional belief bases for which such problem sizes are feasible.