Next: Minimal Model Reasoning Up: Applications Previous: Applications

## 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.

Definition 12 (Kernel)   Let be a graph. A kernel of is a set such that, denoting , it holds:
1. is a vertex cover of
2. 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.

Theorem 8   The problem of inference for the Stable Model semantics is coNP-complete, thus Stable Model Semantics is thm-coNPcomplete.

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:

 (1)

Observe that contains all such that , and in order to be stable, -- i.e., to support atoms such that -- contains no atom such that .

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:
 (2) (3) (4)

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 .

Next: Minimal Model Reasoning Up: Applications Previous: Applications
Paolo Liberatore
2000-07-28