R26  
Default reasoning using classical logic
Rachel BenEliyahu(rachel@cs.ucla.edu) &
Rina Dechter (dechter@ics.uci.edu)

Abstract In this paper we show how propositional default theories can be characterized by classical propositional theories: for each finite default theory, we show a classical propositional theory such that there is a onetoone correspondence between models for the latter and extensions of the former. This means that computing extensions and answering queries about coherence, setmembership and setentailment are reducible to propositional satisfiability. The general transformation is exponential but tractable for a subset which we call 2DT  a superset of network default theories and disjunctionfree default theories. Consequently, coherence and setmembership for the class 2DT is NPcomplete and setentailment is coNPcomplete. This work paves the way for the application of decades of research on efficient algorithms for the satisfiability problem to default reasoning. For example, since propositional satisfiability can be regarded as a constraint satisfaction problem (CSP), this work enables us to use CSP techniques for default reasoning. To illustrate this point we use the taxonomy of tractable CSPs to identify new tractable subsets for Reiter's default logic. Our procedures allow also for computing stable models of extended logic programs. [ps] [pdf] 