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 ($a$ is a letter):

$$M \models_{GCWA} KB ~\mbox{iff~} M \models KB \cup \{\neg a ... ...B \not\vdash \gamma$\ then $KB \not\vdash \gamma \vee a \}$\ }$$

We can now present the results for these two formalisms.

Theorem 9   The problem of model checking for Circumscription is $\parallel\!\leadsto$ 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 $\parallel\!\leadsto$ coNP-complete.

Theorem 10   The problem of model checking for GCWA is in $\parallel\!\leadsto$ P, thus GCWA is in model-P.

Proof. As already pointed out [11], it is possible to rewrite $GCWA(T)$ into a propositional formula $F$ such that, for any given model $M$, $M \models GCWA(T)$ if and only if $M \models F$. Moreover, the size of $F$ is polynomially bounded by the size of $T$. 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 $\parallel\!\leadsto$$\Pi^p_{2}$-complete, thus Circumscription is thm-$\Pi^p_{2}$-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 $\parallel\!\leadsto$$\Pi^p_{2}$-complete.

Theorem 12   The problem of inference for GCWA is $\parallel\!\leadsto$ coNP-complete, thus GCWA is thm-coNP-complete.

Proof. As already pointed out in the proof of Theorem 10, it is possible to rewrite $GCWA(T)$ into a formula $F$ that is equivalent to it. As a consequence, a formula $\alpha$ is a theorem of $GCWA(T)$ if and only if it is a theorem of $F$. 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.