Nonmonotonic Reasoning: Towards efficient calculi and implementations

Abstract

In this paper we do not want to give a detailed overview of the various formalizations of nonmonotonic reasoning that have evolved (those can be found in various textbooks), but we want to give an overview of the main computational techniques and methods leading to implementions of nonmonotonic reasoning. We first introduce the main nonmonotonic logics: \emph{Default Logic}, \emph{Circumscription} and \emph{Autoepistemic Logic}. We also consider the abstract approach of Kraus, Lehmann and Magidor to associate with any reasoning system an \emph{abstract consequence relation}. Then we investigate universal methods for computing in general nonmonotonic logics. We do this with a special eye on the underlying complexity and show how this lead to automated theorem proving in such logics. Finding efficient computation mechanisms for the logics introduced in the former section is the aim of the next Section. There we consider techniques that originated from automated reasoning in first-order predicate calculus. We depict how these techniques can be applied for disjunctive logic programming with programs with variables but only limited use of negation. In particular, we handle \ie{GCWA} as a basis for nonmonotonic negation therein. We then give a declarative overview on nonmonotonicity in logic programming. We introduce (nonmonotonic) semantics of logic programs with negation and disjunction, notably the well-founded and the stable semantics and their extensions to programs containing disjunction--- they constitute the most important semantics and are in close relation to the logics introduced in the next Section. While in we considered in a former section techniques that can be successfully applied for programs with variables and only limited use of negation, we also treat propositional programs with full negation and disjunction. In particular, we provide implementations of \mbox{D-WFS}\Index{D-WFS} and \ie{D-ST ABLE} in polynomial space. We end with a section where we consider the problem of finding good benchmarks to test and compare nonmonotonic systems against. Also cross-referenced as UMIACS-TR-99-48