Model Checking for Nonmonotonic Logics: Algorithms and Complexity

Abstract

. We study the complexity of model checking in propositional nonmonotonic logics. Specically, we rst dene the problem of model checking in such formalisms, based on the fact that several nonmonotonic logics make use of interpretation structures (i.e. default extensions, stable expansions, universal Kripke models) which are more complex than standard interpretations of propositional logic. Then, we analyze the complexity of checking whether a given interpretation structure satises a nonmonotonic theory. In particular, we characterize the complexity of model checking for Reiter's default logic and its restrictions, Moore's autoepistemic logic, and several nonmonotonic modal logics. The results obtained show that, in all such formalisms, model checking is computationally easier than logical inference. 1 Introduction In recent years the problem of model checking has been widely studied in knowledge representation and AI [10, 8]. Informally, model checking for a logical for...