34
Mathematical Aspects of Logic Programming Semantics
Proof: (a) Supportedness of stable models follows immediately from the definition. The supported model {p} for Program 2.3.1 is not stable.
(b) Let P be a program, let M be a stable model for P , and let l be
a level mapping with respect to which M is well-supported. Assume that
K is a model for P with K ⊂ M . Then there exists A ∈ M \ K, and
we can assume without loss of generality that A is also such that l(A) is
minimal. By the well-supportedness of M , there is a clause C of the form
A ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B k in ground(P ) such that for i = 1, . . . , n and
j = 1, . . . , k we have A i ∈ M , l(A) > l(A i ) and B j ∈ M . Since K ⊂ M , we
obtain, for j = 1, . . . k, that B j ∈ K, and by minimality of l(A) we obtain
A i ∈ K for i = 1, . . . , n. Since K is a model for P and the body of C is true
with respect to K, we conclude that A ∈ K, which contradicts the assumption
that A ∈ M \ K. Hence, M must be a minimal model.
In the opposite direction, Program 2.3.5 below has {p} as its only model,
and hence, this is a minimal model. It is clearly not a stable model, however.
(c) By Proposition 2.3.2, we see that the least model is indeed stable.
Uniqueness follows from (b) and Theorem 2.2.3 (c).
•
There are programs with unique supported models which are not stable.
2.3.5 Program The program P consisting of the two clauses
p ← p
p ← ¬p
has unique supported model {p}, and this model is not stable.
A unique stable model is always a least model by Theorem 2.3.4 (b). If a
program has a least model, however, this model is not guaranteed to be stable,
as Program 2.3.5 shows in having {p} as its only model.
A characterization of stable models as fixed points of an operator can be
given, and we proceed with this next.
2.3.6 Definition Let P be a normal logic program, and let I ∈ I P . The
Gelfond–Lifschitz transform P/I of P is the set of all clauses A ← A 1 , . . . , A n
for which there exists a clause A ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B k in ground(P )
with B 1 , . . . , B k ∈ I.
We note that the Gelfond–Lifschitz transform P/I of a program P is always
definite (as a set of ground clauses) and therefore has a least model T P/I ↑ ω
by Theorem 2.2.3. The operator GL P : I � → T P/I ↑ ω is called the Gelfond–
Lifschitz operator
9 associated with P .
2.3.7 Theorem The following hold.
9 The Gelfond–Lifschitz operator is named after the authors of the well-known paper
[Gelfond and Lifschitz, 1988] and was introduced by them in defining the stable model semantics.
Mathematical Aspects of Logic Programming Semantics
Proof: (a) Supportedness of stable models follows immediately from the definition. The supported model {p} for Program 2.3.1 is not stable.
(b) Let P be a program, let M be a stable model for P , and let l be
a level mapping with respect to which M is well-supported. Assume that
K is a model for P with K ⊂ M . Then there exists A ∈ M \ K, and
we can assume without loss of generality that A is also such that l(A) is
minimal. By the well-supportedness of M , there is a clause C of the form
A ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B k in ground(P ) such that for i = 1, . . . , n and
j = 1, . . . , k we have A i ∈ M , l(A) > l(A i ) and B j ∈ M . Since K ⊂ M , we
obtain, for j = 1, . . . k, that B j ∈ K, and by minimality of l(A) we obtain
A i ∈ K for i = 1, . . . , n. Since K is a model for P and the body of C is true
with respect to K, we conclude that A ∈ K, which contradicts the assumption
that A ∈ M \ K. Hence, M must be a minimal model.
In the opposite direction, Program 2.3.5 below has {p} as its only model,
and hence, this is a minimal model. It is clearly not a stable model, however.
(c) By Proposition 2.3.2, we see that the least model is indeed stable.
Uniqueness follows from (b) and Theorem 2.2.3 (c).
•
There are programs with unique supported models which are not stable.
2.3.5 Program The program P consisting of the two clauses
p ← p
p ← ¬p
has unique supported model {p}, and this model is not stable.
A unique stable model is always a least model by Theorem 2.3.4 (b). If a
program has a least model, however, this model is not guaranteed to be stable,
as Program 2.3.5 shows in having {p} as its only model.
A characterization of stable models as fixed points of an operator can be
given, and we proceed with this next.
2.3.6 Definition Let P be a normal logic program, and let I ∈ I P . The
Gelfond–Lifschitz transform P/I of P is the set of all clauses A ← A 1 , . . . , A n
for which there exists a clause A ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B k in ground(P )
with B 1 , . . . , B k ∈ I.
We note that the Gelfond–Lifschitz transform P/I of a program P is always
definite (as a set of ground clauses) and therefore has a least model T P/I ↑ ω
by Theorem 2.2.3. The operator GL P : I � → T P/I ↑ ω is called the Gelfond–
Lifschitz operator
9 associated with P .
2.3.7 Theorem The following hold.
9 The Gelfond–Lifschitz operator is named after the authors of the well-known paper
[Gelfond and Lifschitz, 1988] and was introduced by them in defining the stable model semantics.