The InfOCF Library for Reasoning With Conditional Belief Bases
摘要
This paper presents an overview of the Python library InfOCF that provides powerful tools for working with conditional belief bases consisting of defeasible rules of the form “If A, then usually B”. Because many operations on belief bases, like checking their consistency or performing nonmonotonic reasoning for answering queries, require solving propositional satisfiability problems and generalizations thereof, InfOCF builds upon the power of current SMT and MaxSAT solvers. For achieving solver independence, established interfaces like PySMT are used, allowing the user to select from different solvers. Multiple queries can be run in parallel for speeding up the answering process. Besides its rigorous focus on modularity and extensibility, further notable features of InfOCF include comprehensive methods for caching program states enabling the reuse of intermediate results across different queries to the same belief base. Successful applications realized with, and now available in, InfOCF cover state-of-the-art implementations of nonmonotonic reasoning with p-entailment, system Z, lexicographic inference, c-inference, and system W; each of these implementations scales up and outperforms all previous implementations of the corresponding inference operator by an order of magnitude.