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  and the Generalized Closed World Assumption (GCWA) , 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.
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.
Proof. As already pointed out , 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.
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.
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.