Propositional default logics made easier: computational complexity of model checking

AbstractLiberatore and Schaerf (Proceedings of the ECAI’ 98, 1998) give a proof that model checking for propositional normal default theories is in Δ2P and Δ2P[O(logn)]-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 Δ2P[O(logn)]. 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=Σ2P. Finally, we give an overview of our results concerning model checking in case of disjunctive default logic and stationary default logic