On the Model Checking Complexity of Circumscription

The computational problem of model checking for circumscription of firstorder formulae is studied. We study in which subclasses of circumscriptive predicate formulas there are formulas with coNP-complete model checking problem. We deal with naturally arising subclasses defined in terms of quantifiers prefixes and arities of both circumscribed and uncircumscribed predicates. The formulas with unary circumscribed predicates having intractable model checking problem are demonstrated. The theorem generalizing above intractability results is presented. key words: circumscription, model checking, finite models, computational complexity 1 Introduction Usually when reasoning, one has in mind certain implicit assumptions about the subject of the reasoning. For instance, nearly always the world we reason about is assumably as normal as possible, or, in other words , we assume minimality of its abnormal properties. Circumscription is a formalism of common-sense reasoning, making allowance for ..