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 disjunction-free default theories. Consequently, coherence and set-membership for the class 2-DT is NP-complete and set-entailment is co-NP-complete.