Default reasoning using classical logic

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 one-to-one correspondence between models for the latter and extensions of the former. This means that computing extensions and answering queries about coherence, set-membership and set-entailment are reducible to propositional satisfiability. The general transformation is exponential but tractable for a subset which we call 2-DT-a superset of network default theories and disfunction-free default theories, Consequently, coherence and set-membership for the class 2-DT is NP-complete and set-entailment is co-NP-complete. 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.