35
The Semantics of Logic Programs
(a) The Gelfond–Lifschitz operator is antitonic and, in general, is not monotonic.
(b) An interpretation I is a stable model for a program P if and only if it is
a fixed point of GL P , that is, if and only if it satisfies GL P (I) = I.
Proof: (a) Let P be a program, and let I, K be interpretations for P with
I ⊆ K. Then P/K ⊆ P/I, and it is a straightforward proof by induction to
show that T P/K ↑ n ⊆ T P/I ↑ n for all n ∈ N. Hence, GL P (K) = T P/K ↑ ω ⊆
T P/I ↑ ω = GL P (I), which shows that GL P is antitonic. To see that it is not
generally monotonic, take P to be Program 2.3.5. On setting I = ∅, we obtain
that P/I is the definite program consisting of the clauses p ← p and p ←, and
GL P (I) = {p}; on setting I = {p}, we obtain that P/I consists of the single
clause p ← p, and GL P (I) = ∅. This establishes (a).
For (b), we start by supposing that GL P (I) = T P/I ↑ ω = I. Then I is
the least model for P/I, and hence, is also a model for P , and, by Proposition 2.3.2, is well-supported with respect to any level mapping l satisfying
l(A) = min{n | A ∈ T P/I ↑ (n + 1)} for each A ∈ I. Conversely, let I be
a stable model for P . Then I is well-supported relative to some level mapping l, say. Thus, for every A ∈ I, there is a clause C in ground(P ) of the
form A ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B k such that the body of C is true in I and
l(A i ) < l(A) for i = 1, . . . , n. But then, for every A ∈ I, there is a clause
A ← A 1 , . . . , A n in P/I whose body is true in I and such that l(A i ) < l(A)
for i = 1, . . . , n. By Proposition 2.3.2, this means that I is the least model for
P/I, that is, I = T P/I ↑ ω = GL P (I).
•
The Gelfond–Lifschitz transform can be considered as a two-step process:
first, delete each ground clause which has a negative literal ¬B in its body
with B ∈ I; second, delete all negative literals in the bodies of the remaining
clauses. Indeed, the intuition behind it is as follows. We can think of P as a
set of premises and of I as a set of beliefs that a rational agent might hold and
wants to test, given the premises P . Any ground clause that contains ¬B in its
body, where B ∈ I, is useless to the agent and can be discarded. Among the
remaining ground clauses, an occurrence of ¬B with B ∈ I is trivial. Thus,
we can simplify the premises to P/I. If I happens to be the set of atoms that
logically follow from P/I, then the agent is rational.
We will now give some examples.
2.3.8 Example Consider again Tweety1 from Program 2.1.2 and its supported model M as given in Example 2.2.7. We show that M is stable. The
The Semantics of Logic Programs
(a) The Gelfond–Lifschitz operator is antitonic and, in general, is not monotonic.
(b) An interpretation I is a stable model for a program P if and only if it is
a fixed point of GL P , that is, if and only if it satisfies GL P (I) = I.
Proof: (a) Let P be a program, and let I, K be interpretations for P with
I ⊆ K. Then P/K ⊆ P/I, and it is a straightforward proof by induction to
show that T P/K ↑ n ⊆ T P/I ↑ n for all n ∈ N. Hence, GL P (K) = T P/K ↑ ω ⊆
T P/I ↑ ω = GL P (I), which shows that GL P is antitonic. To see that it is not
generally monotonic, take P to be Program 2.3.5. On setting I = ∅, we obtain
that P/I is the definite program consisting of the clauses p ← p and p ←, and
GL P (I) = {p}; on setting I = {p}, we obtain that P/I consists of the single
clause p ← p, and GL P (I) = ∅. This establishes (a).
For (b), we start by supposing that GL P (I) = T P/I ↑ ω = I. Then I is
the least model for P/I, and hence, is also a model for P , and, by Proposition 2.3.2, is well-supported with respect to any level mapping l satisfying
l(A) = min{n | A ∈ T P/I ↑ (n + 1)} for each A ∈ I. Conversely, let I be
a stable model for P . Then I is well-supported relative to some level mapping l, say. Thus, for every A ∈ I, there is a clause C in ground(P ) of the
form A ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B k such that the body of C is true in I and
l(A i ) < l(A) for i = 1, . . . , n. But then, for every A ∈ I, there is a clause
A ← A 1 , . . . , A n in P/I whose body is true in I and such that l(A i ) < l(A)
for i = 1, . . . , n. By Proposition 2.3.2, this means that I is the least model for
P/I, that is, I = T P/I ↑ ω = GL P (I).
•
The Gelfond–Lifschitz transform can be considered as a two-step process:
first, delete each ground clause which has a negative literal ¬B in its body
with B ∈ I; second, delete all negative literals in the bodies of the remaining
clauses. Indeed, the intuition behind it is as follows. We can think of P as a
set of premises and of I as a set of beliefs that a rational agent might hold and
wants to test, given the premises P . Any ground clause that contains ¬B in its
body, where B ∈ I, is useless to the agent and can be discarded. Among the
remaining ground clauses, an occurrence of ¬B with B ∈ I is trivial. Thus,
we can simplify the premises to P/I. If I happens to be the set of atoms that
logically follow from P/I, then the agent is rational.
We will now give some examples.
2.3.8 Example Consider again Tweety1 from Program 2.1.2 and its supported model M as given in Example 2.2.7. We show that M is stable. The