Next: Default Logic Up: Applications Previous: Stable Model Semantics

## Minimal Model Reasoning

One of the most successful form of non-monotonic reasoning is based on the selection of minimal models. Among the various formalisms based on minimal model semantics we consider here Circumscription [41] and the Generalized Closed World Assumption (GCWA) [42], which is a formalism to represent knowledge in a closed world.

We assume that the reader is familiar with Circumscription, we briefly present the definition of GCWA. The model semantics for GCWA is defined as ( is a letter):

We can now present the results for these two formalisms.

Theorem 9   The problem of model checking for Circumscription is coNP-complete, thus Circumscription is model-coNP-complete.

This result is a trivial corollary of a theorem already proved [11, Theorem 6]. In fact, that proof implicitly shows that model checking for circumscription is coNP-complete.

Theorem 10   The problem of model checking for GCWA is in P, thus GCWA is in model-P.

Proof. As already pointed out [11], it is possible to rewrite into a propositional formula such that, for any given model , if and only if . Moreover, the size of is polynomially bounded by the size of . As a consequence, the model compactness for GCWA is in the same class of PL. By Theorem 3 the thesis follows.

Theorem 11   The problem of inference for Circumscription is -complete, thus Circumscription is thm--complete.

This result is a trivial corollary of a theorem published in a previous paper [11, Theorem 7] which implicitly shows that inference for circumscription is -complete.

Theorem 12   The problem of inference for GCWA is coNP-complete, thus GCWA is thm-coNP-complete.

Proof. As already pointed out in the proof of Theorem 10, it is possible to rewrite into a formula that is equivalent to it. As a consequence, a formula is a theorem of if and only if it is a theorem of . Thus, GCWA has at most the theorem compexity of PL. Since GCWA is a generalization of PL, it follows that GCWA is in the same theorem compactness class of PL. Hence, GCWA is thm-coNP-complete.

Next: Default Logic Up: Applications Previous: Stable Model Semantics
Paolo Liberatore
2000-07-28