53
The Semantics of Logic Programs
L 1 , . . . , L n is true in N , and, since N is a model for L(P ), we obtain A ∈ N ,
which contradicts our assumption.
Now let A ∈ N be an atom with A ∈ I
' , and assume without loss of
generality that A is chosen such that n is minimal with A ∈ T L(P ) ↑ (n + 1).
Then there is a definite clause A ← body in L(P ) such that all atoms in
body are true with respect to T L(P ) ↑ n. Hence, these atoms are also true with
'
respect to I
' , and, since I is a model for L(P ), we obtain A ∈ I
' , which
contradicts our assumption.
Finally, let ¬A ∈ I
' . Then we cannot have A ∈ N ; otherwise, A ∈ I
' . So,
¬A ∈ N since N is a total model for L(P ).
(d) From Lemma 2.5.11, we know that P/N � N P . We distinguish two
cases.
Case i. If A ∈ I \ N , then there must be a clause A ← L 1 , . . . , L k in P such
that L i ∈ I and l(A) > l(L i ) for all i. Since it is not possible for A to belong
to N , there must also be a clause in P/N which subsumes A ← L 1 , . . . , L k
and which therefore satisfies (WSi). So, A satisfies (WSi).
Case ii. If ¬A ∈ I \ N , then, for each clause A ← body1 in P/N , there
must be a clause A ← body in P which is subsumed by A ← body1, and, since
¬A ∈ I, we obtain that condition (WSii) must be satisfied by A and also by
the clause A ← body. Since reduction with respect to N removes only body
literals which are true in N , condition (WSii) is still fulfilled.
•
We can now proceed with the proof of Theorem 2.5.9.
Proof of Theorem 2.5.9: The proof will proceed by establishing the following facts: (1) P satisfies (WS) with respect to M P and l P . (2) If I is a
model for P and l is an I-partial level mapping such that P satisfies (WS)
with respect to I and l, then I ⊆ M P .
(1) Let A ∈ dom(l P ), and suppose that l P (A) = (α, n). We consider two
cases.
Case i. A ∈ M P . Then A ∈ T Lα ↑ (n + 1). Hence, there is a definite clause
A ← A 1 , . . . , A k in L α with A 1 , . . . , A k ∈ T Lα ↑ n. Thus, A 1 , . . . , A k ∈ M P and
l P (A) > l P (A i ) for all i. By Lemma 2.5.11, P/N α � Nα P . So there must be a
clause A ← A 1 , . . . , A k , L 1 , . . . , L m in P with literals L 1 , . . . , L m ∈ N α ⊆ M P ,
and we obtain l P (L j ) < l P (A) for all j = 1, . . . , m. So, (WSi) holds in this
case.
Case ii. ¬A ∈ M P . Let A ← A 1 , . . . , A k , ¬B 1 , . . . , ¬B m be a clause in
P , noting that (WSii) is trivially satisfied in case no such clause exists. We
consider the following two subcases.
Subcase ii.a. Assume A is undefined in N α and was eliminated from P by
reducing it with respect to N α , that is, A ∈ R α . Then, in particular, there
must be some ¬A i ∈ N α , or some B j ∈ N α , which yields l P (A i ) < l P (A), or
l P (B j ) < l P (A), respectively, and hence one of (WSiia), (WSiic) holds.
Subcase ii.b. Assume ¬A ∈ H, where H is the three-valued model corresponding to the least two-valued model for L α . Since P/N α subsumes P
The Semantics of Logic Programs
L 1 , . . . , L n is true in N , and, since N is a model for L(P ), we obtain A ∈ N ,
which contradicts our assumption.
Now let A ∈ N be an atom with A ∈ I
' , and assume without loss of
generality that A is chosen such that n is minimal with A ∈ T L(P ) ↑ (n + 1).
Then there is a definite clause A ← body in L(P ) such that all atoms in
body are true with respect to T L(P ) ↑ n. Hence, these atoms are also true with
'
respect to I
' , and, since I is a model for L(P ), we obtain A ∈ I
' , which
contradicts our assumption.
Finally, let ¬A ∈ I
' . Then we cannot have A ∈ N ; otherwise, A ∈ I
' . So,
¬A ∈ N since N is a total model for L(P ).
(d) From Lemma 2.5.11, we know that P/N � N P . We distinguish two
cases.
Case i. If A ∈ I \ N , then there must be a clause A ← L 1 , . . . , L k in P such
that L i ∈ I and l(A) > l(L i ) for all i. Since it is not possible for A to belong
to N , there must also be a clause in P/N which subsumes A ← L 1 , . . . , L k
and which therefore satisfies (WSi). So, A satisfies (WSi).
Case ii. If ¬A ∈ I \ N , then, for each clause A ← body1 in P/N , there
must be a clause A ← body in P which is subsumed by A ← body1, and, since
¬A ∈ I, we obtain that condition (WSii) must be satisfied by A and also by
the clause A ← body. Since reduction with respect to N removes only body
literals which are true in N , condition (WSii) is still fulfilled.
•
We can now proceed with the proof of Theorem 2.5.9.
Proof of Theorem 2.5.9: The proof will proceed by establishing the following facts: (1) P satisfies (WS) with respect to M P and l P . (2) If I is a
model for P and l is an I-partial level mapping such that P satisfies (WS)
with respect to I and l, then I ⊆ M P .
(1) Let A ∈ dom(l P ), and suppose that l P (A) = (α, n). We consider two
cases.
Case i. A ∈ M P . Then A ∈ T Lα ↑ (n + 1). Hence, there is a definite clause
A ← A 1 , . . . , A k in L α with A 1 , . . . , A k ∈ T Lα ↑ n. Thus, A 1 , . . . , A k ∈ M P and
l P (A) > l P (A i ) for all i. By Lemma 2.5.11, P/N α � Nα P . So there must be a
clause A ← A 1 , . . . , A k , L 1 , . . . , L m in P with literals L 1 , . . . , L m ∈ N α ⊆ M P ,
and we obtain l P (L j ) < l P (A) for all j = 1, . . . , m. So, (WSi) holds in this
case.
Case ii. ¬A ∈ M P . Let A ← A 1 , . . . , A k , ¬B 1 , . . . , ¬B m be a clause in
P , noting that (WSii) is trivially satisfied in case no such clause exists. We
consider the following two subcases.
Subcase ii.a. Assume A is undefined in N α and was eliminated from P by
reducing it with respect to N α , that is, A ∈ R α . Then, in particular, there
must be some ¬A i ∈ N α , or some B j ∈ N α , which yields l P (A i ) < l P (A), or
l P (B j ) < l P (A), respectively, and hence one of (WSiia), (WSiic) holds.
Subcase ii.b. Assume ¬A ∈ H, where H is the three-valued model corresponding to the least two-valued model for L α . Since P/N α subsumes P