InfOCF-Web
A tool for reasoning with conditional knowledge basesDefault rules of the form "If A, then usually B" are powerful constructs for knowledge representation. Such rules can be formalized as conditionals, denoted by (B|A). A conditional knowledge base consists of a set of conditionals. Different semantical models have been proposed for conditional knowledge bases, including quantitative, semi-quantitative, and qualitative approaches. E.g., an ordinal conditional function (OCF) [Spohn, 1988], ordering possible worlds according to their degree of surprise, accepts the conditional (B|A) if it considers a world where A holds, but B does not hold, to be strictly more surprising than a world where both A and B are true.
The most important reasoning problem for conditional knowledge bases is to determine which consequences a knowledge base entails. Some of the approaches to specifying the entailments of a conditional knowledge base are system P [Lehmann and Magidor, 1992] taking all models into account, system Z [Pearl, 1990] taking the unique minimal OCF into account, inference with respect to a single c-representation [Kern-Isberner, 2001 (LNCS), Kern-Isberner, 2004 (AMAI)], c-inference relations realizing various modes of inference and taking different classes of c-representations into account [Beierle et al., 2016 (FoIKS), Beierle et al., 2016 (ECAI), Beierle et al., 2018 (AMAI), Beierle et al., 2021 (AIJ)], or system W that extends both system Z and c-inference [Komo, Beierle 2020 (KI), Komo, Beierle 2020 (AMAI)].
InfOCF-Web is a tool for reasoning with conditional knowledge bases. The objective of InfOCF-Web is to provide an easy-to-use online tool for computing and comparing a variety of different inference relations induced by a knowledge base. For background information and for the formal definition of the inductive inference operators realized by InfOCF-Web, we refer to the papers cited on this page and to the list of publications given here.
The current version of InfOCF-Web is InfOCF-Web 2.0. For solving the satisfaction and constraint satisfiability problems underlying the different inference operators, current SAT and SMT solvers are employed [Beierle et al., 2022 (FLAIRS), von Berg et al., 2022 (ECSQARU), von Berg et al., 2024 (FoIKS), Beierle et al., 2024 (FLAIRS)]. InfOCF-Web 2.0 scales up reasoning from conditional knowledge bases significantly, allowing for signatures of 100+ propositional variables and knowledge bases containing 100+ propositional variables.
The previous version of InfOCF-Web [Kutsch, Beierle 2021 (IJCAI)] is implemented using the Java library InfOCF-Lib [Kutsch, 2019], providing sophisticated representation and reasoning methods for conditional logic and ranking functions [Kutsch, 2020], and a Prolog backend, providing a constraint satisfaction problem solver [Beierle et al., 2017 (KI)].
It was later extended by a first implementation of system W [Beierle et al., 2022 (KI)].
Feedback
We welcome your feedback regarding this tool. Please send us your comments and hints by email: christoph.beierle@fernuni-hagen.de
References
—