Stable model semantics ( SM) was introduced by Gelfond and Lifschitz  as a tool to provide a semantics for logic programs with negation. their original proposal is now one of the standard semantics for logic programs. We now recall the definition of propositional stable model.
Let be a propositional, general logic program. Let be a subset (i.e., an interpretation) of the atoms of . Let be the program obtained from in the following way: if a clause of contains in its body a negated atom such that then is deleted; if a body of a clause contains a negated atom such that then is deleted from the body of the clause. If is a least Herbrand model of then is a stable model of .
For the formalism SM, we consider the program as the knowledge base. We write to denote that query is implied by a logic program under Stable Model semantics.
In order to prove our result, we need to define the kernel of a graph.
We can now state the theorem on the compilability class of inference in the stable model semantics, and the corresponding theorem compactness class.
Proof. Membership in the class follows from the fact that the problem is coNP-complete . For the hardness, we adapt the proof of Marek and Truszczynski  showing that deciding whether a query is true in all stable models is coNP-hard.
Let KERNEL be the language such that is a graph with at least one kernel. Let , and observe that cannot have more vertices than its size .
We show that for each , there exists a logic program such that for every graph with at most vertices, there exists a query such that has a kernel iff .
Let the alphabet of be composed by the following propositional letters: .
The program is defined as:
As a result, this is a reduction. We now show that this reduction is correct, i.e., KERNEL ( has a kernel) iff .
. Then, there
exists a stable model of such that
Observe that is equivalent to the conjunction of all
such that , and all such that
. Simplifying with we obtain
Let , . Now is a vertex cover of G, since for each edge , should satisfy the corresponding clause (1) , hence either , or . Moreover, for each in , the atom is in , and since is a stable model, there exists a clause such that , that is, . Therefore, is a kernel of .
Only-if part. Suppose has a kernel , and let
. Let be the interpretation