63
The Semantics of Logic Programs
then l(A) > l(B j ). Otherwise, since A ∈ T P/Lα ↑ ω, we have that there exists
A i with A i ∈ T P/Lα ↑ ω, and hence l(A) ≥ l(A i ), and this suffices.
This finishes the proof that P satisfies (WF) with respect to M and l. It
therefore only remains to show that M is greatest with this property.
So assume that M 1 = M is the greatest model such that P satisfies (WF)
with respect to M 1 and some M 1 -partial level mapping l 1 .
Assume L ∈ M 1 \ M , and, without loss of generality, let the literal L be
chosen such that l 1 (L) is minimal. We consider the following two cases.
Case i. If L = A is an atom, then there exists a clause A ← body in
ground(P ) such that body is true in M 1 and l 1 (L) < l 1 (A) for all literals
L in body. Hence, body is true in M , and A ← body transforms to a clause
A ← A 1 , . . . , A n in P/G P with A 1 , . . . , A n ∈ L P = T P/G P ↑ ω. But this implies
A ∈ M , contradicting A ∈ M 1 \ M .
Case ii. If L = ¬A ∈ M 1 \ M is a negated atom, then ¬A ∈ M 1 and
A ∈ G P = T P/L P ↑ ω, so A ∈ T P/L P ↑ n for some n ∈ N. We show by induction
on n that this leads to a contradiction to finish the proof.
If A ∈ T P/L P ↑ 1, then there is a unit clause A ← in P/L P , and any
corresponding clause A ← ¬B 1 , . . . , ¬B k in ground(P ) satisfies B 1 , . . . , B k ∈
L P . Since ¬A ∈ M 1 , we also obtain by Theorem 2.6.8 that there is i ∈
{1, . . . , k} such that B i ∈ M 1 and l 1 (B i ) < l 1 (A). By minimality of l 1 (A), we
obtain B i ∈ M , and hence B i ∈ L P , which contradicts B i ∈ L P .
Now assume that there is no ¬B ∈ M 1 \ M with B ∈ T P/L P ↑ k for any
k < n + 1, and let ¬A ∈ M 1 \ M with A ∈ T P/L P ↑ (n + 1). Then there is a
clause A ← A 1 , . . . , A m in P/L P with A 1 , . . . , A m ∈ T P/L P ↑ n ⊆ G P , and we
note that we cannot have ¬A i ∈ M 1 \ M for any i ∈ {1, . . . , m} by our current
induction hypothesis. Furthermore, it is also impossible for ¬A i to belong to
M for any i; otherwise, we would have A i ∈ B P \ G P . Thus, we conclude
that we cannot have ¬A i ∈ M 1 for any i. Moreover, there is a corresponding
clause A ← A 1 , . . . , A m , ¬B 1 , . . . , ¬B m1 in ground(P ) with B 1 , . . . , B m1 ∈
L P . Hence, by Theorem 2.6.8, we know that there is i ∈ {1, . . . , m 1 } such
that B i ∈ M 1 and l 1 (B i ) < l 1 (A). By minimality of l 1 (A), we conclude that
B i ∈ M , so that B i ∈ L P , and this contradicts B i ∈ L P .
•
It follows from Theorem 2.6.13 (b) that total well-founded models are
unique stable models. The converse, however, does not hold. Indeed, Program
2.4.14 has well-founded model ∅, as can easily be seen by noting that GL P (∅) =
B P and GL P (B P ) = ∅.
2.6.14 Theorem Let P be a program with a total Fitting model. Then P
has a total well-founded model and a total weakly perfect model. Moreover,
P also has a unique stable and a unique supported model. Furthermore, all
these models coincide.
Proof: By Propositions 2.5.14 and 2.6.10, P has a total well-founded and a
total weakly perfect model, both of which coincide with the Fitting model.
By Theorem 2.6.13 (b), P has a unique stable model, and this coincides with
The Semantics of Logic Programs
then l(A) > l(B j ). Otherwise, since A ∈ T P/Lα ↑ ω, we have that there exists
A i with A i ∈ T P/Lα ↑ ω, and hence l(A) ≥ l(A i ), and this suffices.
This finishes the proof that P satisfies (WF) with respect to M and l. It
therefore only remains to show that M is greatest with this property.
So assume that M 1 = M is the greatest model such that P satisfies (WF)
with respect to M 1 and some M 1 -partial level mapping l 1 .
Assume L ∈ M 1 \ M , and, without loss of generality, let the literal L be
chosen such that l 1 (L) is minimal. We consider the following two cases.
Case i. If L = A is an atom, then there exists a clause A ← body in
ground(P ) such that body is true in M 1 and l 1 (L) < l 1 (A) for all literals
L in body. Hence, body is true in M , and A ← body transforms to a clause
A ← A 1 , . . . , A n in P/G P with A 1 , . . . , A n ∈ L P = T P/G P ↑ ω. But this implies
A ∈ M , contradicting A ∈ M 1 \ M .
Case ii. If L = ¬A ∈ M 1 \ M is a negated atom, then ¬A ∈ M 1 and
A ∈ G P = T P/L P ↑ ω, so A ∈ T P/L P ↑ n for some n ∈ N. We show by induction
on n that this leads to a contradiction to finish the proof.
If A ∈ T P/L P ↑ 1, then there is a unit clause A ← in P/L P , and any
corresponding clause A ← ¬B 1 , . . . , ¬B k in ground(P ) satisfies B 1 , . . . , B k ∈
L P . Since ¬A ∈ M 1 , we also obtain by Theorem 2.6.8 that there is i ∈
{1, . . . , k} such that B i ∈ M 1 and l 1 (B i ) < l 1 (A). By minimality of l 1 (A), we
obtain B i ∈ M , and hence B i ∈ L P , which contradicts B i ∈ L P .
Now assume that there is no ¬B ∈ M 1 \ M with B ∈ T P/L P ↑ k for any
k < n + 1, and let ¬A ∈ M 1 \ M with A ∈ T P/L P ↑ (n + 1). Then there is a
clause A ← A 1 , . . . , A m in P/L P with A 1 , . . . , A m ∈ T P/L P ↑ n ⊆ G P , and we
note that we cannot have ¬A i ∈ M 1 \ M for any i ∈ {1, . . . , m} by our current
induction hypothesis. Furthermore, it is also impossible for ¬A i to belong to
M for any i; otherwise, we would have A i ∈ B P \ G P . Thus, we conclude
that we cannot have ¬A i ∈ M 1 for any i. Moreover, there is a corresponding
clause A ← A 1 , . . . , A m , ¬B 1 , . . . , ¬B m1 in ground(P ) with B 1 , . . . , B m1 ∈
L P . Hence, by Theorem 2.6.8, we know that there is i ∈ {1, . . . , m 1 } such
that B i ∈ M 1 and l 1 (B i ) < l 1 (A). By minimality of l 1 (A), we conclude that
B i ∈ M , so that B i ∈ L P , and this contradicts B i ∈ L P .
•
It follows from Theorem 2.6.13 (b) that total well-founded models are
unique stable models. The converse, however, does not hold. Indeed, Program
2.4.14 has well-founded model ∅, as can easily be seen by noting that GL P (∅) =
B P and GL P (B P ) = ∅.
2.6.14 Theorem Let P be a program with a total Fitting model. Then P
has a total well-founded model and a total weakly perfect model. Moreover,
P also has a unique stable and a unique supported model. Furthermore, all
these models coincide.
Proof: By Propositions 2.5.14 and 2.6.10, P has a total well-founded and a
total weakly perfect model, both of which coincide with the Fitting model.
By Theorem 2.6.13 (b), P has a unique stable model, and this coincides with