Nonmonotonic reasoning in classical logic

Reiter's default logic is one of the most successful formalisms for nonmonotonic reasoning. It has also provided semantics for logic programs with negation, known as stable model semantics. However, a general proof procedure for reasoning in default logic is lacking and the existing inference algorithms are highly complex. This thesis focuses on propositional default logic. We present new semantics for this logic that leads to a propositional characterization of default theories. For each such finite theory, we show a classical propositional theory such that there is a one-to-one correspondence between models for the latter and extensions of the former. This means that computing an extension and answering questions about coherence, set-membership, and set-entailment are reducible to propositional satisfiability. Although the transformation presented here is exponential in general, it is tractable for an important subclass of default theories that includes network default theories and logic programs (under stable model semantics). The proposed reduction suggests that any of a number of algorithms and heuristics known for solving satisfiability can now be used in default reasoning. In particular, tractable propositional theories yield tractable default theories. We illustrate this point by showing how techniques borrowed from the area of constraint-based reasoning can be used to answer queries posed on default theories and to identify new tractable subclasses. We also show how the approach developed here can be applied for computing stable models of extended logic programs and of a major subclass of disjunctive extended logic programs. Finally, we show how our method can be extended to the class of first-order normal logic programs. The extension to the class of first-order programs turns out to be very closely related to Clark's predicate completion for logic programs.