51
The Semantics of Logic Programs
and the set difference {K 1 , . . . , K m } \ {L 1 , . . . , L n } contains only elements of
N α . Condition 3(ii) holds because for each clause C 2 = (A ← K 1 , . . . , K m ) in
P with head A ∈ N α whose body is true under N α , Step 2 in the reduction
of P with respect to N α removes all the body literals K i . Therefore, we have
that C 1 = (A ←) is a fact in P/N α , and clearly, C 1 � C 2 .
•
The next lemma establishes the induction step in Part (2) of the proof of
Theorem 2.5.9.
2.5.12 Lemma If I is a non-empty three-valued model for a (infinite propo'
sitional normal) logic program P and l is an I-partial level mapping such
'
that P satisfies (WS) with respect to I and l, then the following hold for
P = P
' /∅.
(a) The bottom stratum S(P ) of P is non-empty and consists of trivial components only.
(b) The bottom layer L(P ) of P is definite.
(c) The three-valued model N corresponding to the least two-valued model
for L(P ) is consistent with I in the following sense: we have I
' ⊆ N , where
I
' is the restriction of I to all atoms which are not undefined in N .
(d) P/N satisfies (WS) with respect to I \ N and l| N , where l| N is the restriction of l to the atoms in I \ N .
Proof: (a) Assume that there exists some component C ⊆ S(P ) which is
not trivial. Then there must exist atoms A, B ∈ C with A < B, B < A,
and A = B. Without loss of generality, we can assume that A is chosen such
that l(A) is minimal. Now let A
' be any atom occurring in the body of a
clause with head A. If A
' occurs positively, then A > B > A ≥ A
' , and so
A > A
' ; if A
' occurs negatively, then A > A
' also. Therefore, by minimality
of the component, we must also have A
' > A. Thus, we obtain that all atoms
occurring positively or negatively in the bodies of clauses with head A must
be contained in C. We consider two cases.
Case i. If A ∈ I, then there must be a fact A ← in P ; otherwise, by (WSi)
we have a clause A ← L 1 , . . . , L n (for some n ≥ 1) with L 1 , . . . , L n ∈ I and
l(A) > l(L i ) for all i, contradicting the minimality of l(A). Since P = P
' /∅,
we obtain that A ← is the only clause in P with head A, contradicting the
existence of B = A with B < A.
Case ii. If ¬A ∈ I, then since A was chosen to be minimal with respect to l, we obtain that condition (WSiib) must hold for each clause
A ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m with respect to I and l and that m = 0.
Furthermore, all A i must be contained in C, as already noted above, and
l(A) ≥ l(A i ) for all i by (WSiib). Also, from Case i, we obtain that no A i can
be contained in I. We have now established that, for all A i in the body of any
clause with head A, we have l(A) = l(A i ) and ¬A i ∈ I. The same argument
The Semantics of Logic Programs
and the set difference {K 1 , . . . , K m } \ {L 1 , . . . , L n } contains only elements of
N α . Condition 3(ii) holds because for each clause C 2 = (A ← K 1 , . . . , K m ) in
P with head A ∈ N α whose body is true under N α , Step 2 in the reduction
of P with respect to N α removes all the body literals K i . Therefore, we have
that C 1 = (A ←) is a fact in P/N α , and clearly, C 1 � C 2 .
•
The next lemma establishes the induction step in Part (2) of the proof of
Theorem 2.5.9.
2.5.12 Lemma If I is a non-empty three-valued model for a (infinite propo'
sitional normal) logic program P and l is an I-partial level mapping such
'
that P satisfies (WS) with respect to I and l, then the following hold for
P = P
' /∅.
(a) The bottom stratum S(P ) of P is non-empty and consists of trivial components only.
(b) The bottom layer L(P ) of P is definite.
(c) The three-valued model N corresponding to the least two-valued model
for L(P ) is consistent with I in the following sense: we have I
' ⊆ N , where
I
' is the restriction of I to all atoms which are not undefined in N .
(d) P/N satisfies (WS) with respect to I \ N and l| N , where l| N is the restriction of l to the atoms in I \ N .
Proof: (a) Assume that there exists some component C ⊆ S(P ) which is
not trivial. Then there must exist atoms A, B ∈ C with A < B, B < A,
and A = B. Without loss of generality, we can assume that A is chosen such
that l(A) is minimal. Now let A
' be any atom occurring in the body of a
clause with head A. If A
' occurs positively, then A > B > A ≥ A
' , and so
A > A
' ; if A
' occurs negatively, then A > A
' also. Therefore, by minimality
of the component, we must also have A
' > A. Thus, we obtain that all atoms
occurring positively or negatively in the bodies of clauses with head A must
be contained in C. We consider two cases.
Case i. If A ∈ I, then there must be a fact A ← in P ; otherwise, by (WSi)
we have a clause A ← L 1 , . . . , L n (for some n ≥ 1) with L 1 , . . . , L n ∈ I and
l(A) > l(L i ) for all i, contradicting the minimality of l(A). Since P = P
' /∅,
we obtain that A ← is the only clause in P with head A, contradicting the
existence of B = A with B < A.
Case ii. If ¬A ∈ I, then since A was chosen to be minimal with respect to l, we obtain that condition (WSiib) must hold for each clause
A ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m with respect to I and l and that m = 0.
Furthermore, all A i must be contained in C, as already noted above, and
l(A) ≥ l(A i ) for all i by (WSiib). Also, from Case i, we obtain that no A i can
be contained in I. We have now established that, for all A i in the body of any
clause with head A, we have l(A) = l(A i ) and ¬A i ∈ I. The same argument