Stable Model Semantics

Stable model semantics (** SM**) was introduced by Gelfond and Lifschitz
[18] 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.

- is a vertex cover of
- for all , there exists an such that .

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 [40]. For the hardness, we adapt
the proof of Marek and Truszczynski [40] 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:

Given a graph , the query is defined as

The reduction from KERNEL to SM is defined as: , i.e., depends only on its second argument, , i.e., is a constant function, and , i.e., given a graph , the circuit computes the query .

As a result, this is a reduction. We now show that this reduction is correct, i.e., KERNEL ( has a kernel) iff .

*If-part.* Suppose
. 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
the clauses:

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

Obviously, . We now show that is a stable model of , i.e., is a least Herbrand model of . In fact, contains the following clauses:

Clauses in the last line are obtained from clauses in of the form , where the clauses such that (hence ) are deleted, while in the other clauses the negated atom is deleted, since , hence . Now for each , the vertex is in , hence there is an edge , and . Hence clauses (4) and (3) are in , hence in the least Herbrand model of there are exactly all such that .