Propositional default logics made easier: computational complexity of model checking

Liberatore and Schaerf (Proceedings of the ECAI’ 98, 1998) give a proof that model checking for propositional normal default theories is in Δ 2 P and Δ2 P[O(log n)]-hard. However, the precise complexity is left as an open problem. We solve this problem by proving that model checking for normal default theories is complete for Δ2 P[O(log n)]. This is the class of decision problems solvable in polynomial time with a logarithmic number of calls to an oracle in NP. Additionally, we analyse the computational cost of model checking w. r. t. weak extensions, stable expansions and N -expansions and take a look at the complexity of model checking for disjunction-free default theories. Furthermore, we show that not only for disjunction-free default theories, but also for a larger class of default theories, which we call default theories in extended Horn normal form, the complexity of model checking is, in the case of normal default theories, tractable. Additionally, the complexity results are used to draw some interesting conclusions on translatability issues. In particular, there exists no function from default logic into logic programming which is polynomial, faithful and modular unless coNP =Σ2 P. Finally, we give an overview of our results concerning model checking in case of disjunctive default logic and stationary default logic.

Authors

• Robert Baumgartner
• Georg Gottlob

Keywords

• Reiter's default logic
• Normal default theories
• Computational complexity
• Model checking
• EHNF default theories
• Weak extensions