Nonmonotonic Reasoning: Towards efficient calculi and implementations
Nonmonotonic Reasoning: Towards efficient calculi and implementations
No Thumbnail Available
Files
Publication or External Link
Date
1999-09-11
Authors
Dix, Juergen
Furbach, Ulrich
Niemelae, Ilkka
Advisor
Citation
DRUM DOI
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