Nonmonotonic reasoning from conditional knowledge bases with system W

For nonmonotonic reasoning in the context of a knowledge base $\mathcal {R}$ R containing conditionals of the form If A then usually B, system P provides generally accepted axioms. Inference solely based on system P, however, is inherently skeptical because it coincides with reasoning that takes all ranking models of $\mathcal {R}$ R into account. System Z uses only the unique minimal ranking model of $\mathcal {R}$ R , and c-inference, realized via a complex constraint satisfaction problem, takes all c-representations of $\mathcal {R}$ R into account. C-representations constitute the subset of all ranking models of $\mathcal {R}$ R that are obtained by assigning non-negative integer impacts to each conditional in $\mathcal {R}$ R and summing up, for every world, the impacts of all conditionals falsified by that world. While system Z and c-inference license in general different sets of desirable entailments, the first major objective of this article is to present system W. System W fully captures and strictly extends both system Z and c-inference. Moreover, system W can be represented by a single strict partial order on the worlds over the signature of $\mathcal {R}$ R . We show that system W exhibits further inference properties worthwhile for nonmonotonic reasoning, like satisfying the axioms of system P, respecting conditional indifference, and avoiding the drowning problem. The other main goal of this article is to provide results on our investigations, underlying the development of system W, of upper and lower bounds that can be used to restrict the set of c-representations that have to be taken into account for realizing c-inference. We show that the upper bound of n − 1 is sufficient for capturing c-inference with respect to $\mathcal {R}$ R having n conditionals if there is at least one world verifying all conditionals in $\mathcal {R}$ R . In contrast to the previous conjecture that the number of conditionals in $\mathcal {R}$ R is always sufficient, we prove that there are knowledge bases requiring an upper bound of 2n− 1, implying that there is no polynomial upper bound of the impacts assigned to the conditionals in $\mathcal {R}$ R for fully capturing c-inference.

Nonmonotonic Reasoning, Expectations Orderings, and Conceptual Spaces

In Gärdenfors and Makinson (Artif Intell 65(2):197–245, 1994) and Gärdenfors (Knowledge representation and reasoning under uncertainty, Springer-Verlag, 1992) it was shown that it is possible to model nonmonotonic inference using a classical consequence relation plus an expectation-based ordering of formulas. In this article, we argue that this framework can be significantly enriched by adopting a conceptual spaces-based analysis of the role of expectations in reasoning. In particular, we show that this can solve various epistemological issues that surround nonmonotonic and default logics. We propose some formal criteria for constructing and updating expectation orderings based on conceptual spaces, and we explain how to apply them to nonmonotonic reasoning about objects and properties.

as Input Language for Answer Set Solvers

Technological progress in Answer Set Programming (ASP) has been stimulated by the use of common standards, such as the ASP-Core-2 language. While ASP has its roots in nonmonotonic reasoning, efforts have also been made to reconcile ASP with classical first-order (FO) logic. This has resulted in the development of FO(·), an expressive extension of FO, which allows ASP-like problem solving in a purely classical setting. This language may be more accessible to domain experts already familiar with FO and may be easier to combine with other formalisms that are based on classical logic. It is supported by the IDP inference system, which has successfully competed in a number of ASP competitions. Here, however, technological progress has been hampered by the limited number of systems that are available for FO(·). In this paper, we aim to address this gap by means of a translation tool that transforms an FO(·) specification into ASP-Core-2, thereby allowing ASP-Core-2 solvers to be used as solvers for FO(·) as well. We present experimental results to show that the resulting combination of our translation with an off-the-shelf ASP solver is competitive with the IDP system as a way of solving problems formulated in FO(·).

Approximation Fixpoint Theory for Non-Deterministic Operators and Its Application in Disjunctive Logic Programming

Approximation fixpoint theory (AFT) constitutes an abstract and general algebraic framework for studying the semantics of nonmonotonic logics. It provides a unifying study of the semantics of different formalisms for nonmonotonic reasoning, such as logic programming, default logic and autoepistemic logic. In this paper, we extend AFT to non-deterministic constructs such as disjunctive information. This is done by generalizing the main constructions and corresponding results to non-deterministic operators, whose ranges are sets of elements rather than single elements. The applicability and usefulness of this generalization is illustrated in the context of disjunctive logic programming.

Normal forms of conditional knowledge bases respecting system P-entailments and signature renamings

Conditionals are defeasible rules of the form If A then usually B, and they play a central role in many approaches to nonmonotonic reasoning. Normal forms of conditional knowledge bases consisting of a set of such conditionals are useful to create, process, and compare the knowledge represented by them. In this article, we propose several new normal forms for conditional knowledge bases. Compared to the previously introduced antecedent normal form, the reduced antecedent normal form (RANF) represents conditional knowledge with significantly fewer conditionals by taking nonmonotonic entailments licenced by system P into account. The renaming normal form(ρNF) addresses equivalences among conditional knowledge bases induced by renamings of the underlying signature. Combining the concept of renaming normal form with other normal forms yields the renaming antecedent normal form (ρ ANF) and the renaming reduced antecedent normal form (ρ RANF). For all newly introduced normal forms, we show their key properties regarding, existence, uniqueness, model equivalence, and inferential equivalence, and we develop algorithms transforming every conditional knowledge base into an equivalent knowledge base being in the respective normal form. For the most succinct normal form, the ρ RANF, we present an algorithm KBρra systematically generating knowledge bases over a given signature in ρ RANF. We show that the generated knowledge bases are consistent, pairwise not antecedentwise equivalent, and pairwise not equivalent under signature renaming. Furthermore, the algorithm is complete in the sense that, when taking signature renamings and model equivalence into account, every consistent knowledge base is generated. Observing that normalizing the set of all knowledge bases over a signature Σ to ρ RANF yields exactly the same result as KBρra (Σ), highlights the interrelationship between normal form transformations on the one hand and systematically generating knowledge bases in normal form on the other hand.

InfOCF-Web: An Online Tool for Nonmonotonic Reasoning with Conditionals and Ranking Functions

InfOCF-Web provides implementations of system P and system Z inference, and of inference relations based on c-representation with respect to various inference modes and different classes of minimal models. It has an easy-to-use online interface for computing ranking models of a conditional knowledge R, and for answering queries and comparing inference results of nonmonotonic inference relations induced by R.

On the correspondence between abstract dialectical frameworks and nonmonotonic conditional logics

The exact relationship between formal argumentation and nonmonotonic logics is a research topic that keeps on eluding researchers despite recent intensified efforts. We contribute to a deeper understanding of this relation by investigating characterizations of abstract dialectical frameworks in conditional logics for nonmonotonic reasoning. We first show that in general, there is a gap between argumentation and conditional semantics when applying several intuitive translations, but then prove that this gap can be closed when focusing on specific classes of translations.

A Unifying Approach for Nonmonotonic S4F, (Reflexive) Autoepistemic Logic, and Answer Set Programming

This paper presents a general strategy, bringing together some major types of nonmonotonic reasoning under a monotonic bimodal setting. Such formalisms are also of interest to the fields of knowledge representation and declarative programming. We exemplify the methodology, capturing minimal model reasoning that underlies nonmonotonicity over S4F first, but then we also show how to apply the technique to other nonmonotonic logics respectively based on the modal logics KD45 and SW5. We naturally succeed it, by modifying only the axioms of the underlying modal logic and show that it successfully works. The last two formalisms are also known as autoepistemic logic (AEL) and its reflexive extension (RAEL) in the given order: AEL is an important form of nonmonotonic reasoning, introduced by Robert C. Moore in order to allow an agent to reason about his own knowledge. Equilibrium logic (EL) is a general-purpose nonmonotonic reasoning formalism, proposed more recently by David Pearce as a semantical framework for answer set programming (ASP). The latter is an efficient declarative problem solving approach with lots of applications to science and technology. Fariñas et al. have embedded EL (and so ASP) into a monotonic bimodal logic. We take this work as an initiative and successfully apply a similar methodology to closely aligned nonmonotonic modal logics. We finally discuss the potential capability to subsume the epistemic extensions of ASP within our unified paradigm.

Reasoning about Cardinal Directions between 3-Dimensional Extended Objects using Answer Set Programming

We propose a novel formal framework (called 3D-NCDC-ASP) to represent and reason about cardinal directions between extended objects in 3-dimensional (3D) space, using Answer Set Programming (ASP). 3D-NCDC-ASP extends Cardinal Directional Calculus (CDC) with a new type of default constraints, and NCDC-ASP to 3D. 3D-NCDC-ASP provides a flexible platform offering different types of reasoning: Nonmonotonic reasoning with defaults, checking consistency of a set of constraints on 3D cardinal directions between objects, explaining inconsistencies, and inferring missing CDC relations. We prove the soundness of 3D-NCDC-ASP, and illustrate its usefulness with applications.