On the Complexity of Model Checking for Propositional Default Logics: New Results and Tractable Cases

Abstract

We analyse the complexity of standard and weak model checking for propositional default logic; in particular, we solve the open problem of complexity in case of normal default theories and introduce a new ample class of default theories with a tractable model checking problem. 1 Introduction and Overview of Results The complexity of default reasoning is already well understood, however, in search of model-based representations, the complexity of the model checking problem instead of the inference problem needs to be analysed. As Halpern and Vardi [ 1991 ] argue, model checking is a benecial alternative simplifying reasoning tasks (for instance, in classical propositional logic, model checking can be done using an easy polynomial algorithm, however reasoning is coNP-complete) and allowing for representing the agent's knowledge as a semantic structure instead of a collection of formulae and additionally, this approach introduces a kind of closed-world assumption. Furthermore, the...