52
Mathematical Aspects of Logic Programming Semantics
holds for all clauses with head A i , for all i, and the argument repeats itself.
Now, from A > B, we obtain D, E ∈ C with A ≥ E (or A = E), D ≥ B (or
D = B), and E refers negatively to D. As we have just seen, we obtain ¬E ∈ I
and l(E) = l(A). Since E refers negatively to D, there is a clause containing E
in its head and ¬D in its body. Since (WSii) holds for this clause, there must
be a literal L in its body with level less than l(E), so that l(L) < l(A) and
L ∈ C, which is a contradiction. We thus have established that all components
are trivial.
We show next that the bottom stratum is non-empty. Indeed, let A be
an atom such that l(A) is minimal. We will show that {A} is a component.
Assume that this is not the case, that is, assume that there is B with B < A.
Then there exist D 1 , . . . , D k , for some k ∈ N, such that D 1 = A, D j refers
to D j+1 for all j = 1, . . . , k − 1, and D k refers negatively to some B
' with
B
' ≥ B (or B
' = B).
We show by induction that, for all j = 1, . . . , k, the following statements
hold: ¬D j ∈ I, B < D j , and l(D j ) = l(A). Indeed, note that for j = 1, that is,
when D j = A, we have that B < D j = A and l(D j ) = l(A). Assuming A ∈ I,
we obtain, by minimality of l(A), that A ← is the only clause in P = P
' /∅ with
head A, contradicting the existence of B < A. So, ¬A ∈ I, and the assertion
holds for j = 1. Now assume that the assertion holds for some j < k. Then
obviously D j+1 > B since A ≥ D 2 ≥ . . . ≥ D k−1 ≥ D k > B
' ≥ B. Since
¬D j ∈ I and l(D j ) = l(A), we obtain that (WSii) must hold, and, by the
minimality of l(A), we infer that (WSiib) must hold and that no clause with
head D j contains negated atoms. So, l(D j+1 ) = l(D j ) = l(A) holds by (WSiib)
and the minimality of l(A). Furthermore, the assumption D j+1 ∈ I can be
rejected by the same argument as for A above; otherwise, D j+1 ← would be
the only clause with head D j+1 by minimality of l(D j+1 ) = l(A), contradicting
B < D j+1 . This concludes the inductive proof.
Summarizing, we obtain that D k refers negatively to B
' and that ¬D k ∈ I.
But then there is a clause satisfying (WSii) with head D k and ¬B
' in its body,
and this contradicts the minimality of l(D k ) = l(A). This concludes the proof
of statement (a).
(b) Assume that L(P ) is not definite. Then there exists a clause A ← body
in L(P ) with a negated literal ¬B occurring in body. But then B < A, and
since the bottom stratum consists of minimal components only, we also have
A < B, that is, A and B are in the same component, contradicting (a).
'
(c) First, note that in forming the reduct P of P with respect to ∅, the
third step is the only one in the process which has any effect in that it removes
all non-unit clauses whose heads appear also as heads of unit clauses. Now
'
let A ∈ I be an atom with A ∈ N , and assume without loss of generality
that A is chosen such that l(A) is minimal with these properties. By the first
'
observation and the hypothesis that P satisfies (WS) with respect to I and
l, there must be a clause A ← L 1 , . . . , L n in P such that, for all i, L i is true
with respect to I, and hence true with respect to I
' , and l(A) > l(L i ). Hence,
all the literals L i are true with respect to N by minimality of l(A). Thus,
Mathematical Aspects of Logic Programming Semantics
holds for all clauses with head A i , for all i, and the argument repeats itself.
Now, from A > B, we obtain D, E ∈ C with A ≥ E (or A = E), D ≥ B (or
D = B), and E refers negatively to D. As we have just seen, we obtain ¬E ∈ I
and l(E) = l(A). Since E refers negatively to D, there is a clause containing E
in its head and ¬D in its body. Since (WSii) holds for this clause, there must
be a literal L in its body with level less than l(E), so that l(L) < l(A) and
L ∈ C, which is a contradiction. We thus have established that all components
are trivial.
We show next that the bottom stratum is non-empty. Indeed, let A be
an atom such that l(A) is minimal. We will show that {A} is a component.
Assume that this is not the case, that is, assume that there is B with B < A.
Then there exist D 1 , . . . , D k , for some k ∈ N, such that D 1 = A, D j refers
to D j+1 for all j = 1, . . . , k − 1, and D k refers negatively to some B
' with
B
' ≥ B (or B
' = B).
We show by induction that, for all j = 1, . . . , k, the following statements
hold: ¬D j ∈ I, B < D j , and l(D j ) = l(A). Indeed, note that for j = 1, that is,
when D j = A, we have that B < D j = A and l(D j ) = l(A). Assuming A ∈ I,
we obtain, by minimality of l(A), that A ← is the only clause in P = P
' /∅ with
head A, contradicting the existence of B < A. So, ¬A ∈ I, and the assertion
holds for j = 1. Now assume that the assertion holds for some j < k. Then
obviously D j+1 > B since A ≥ D 2 ≥ . . . ≥ D k−1 ≥ D k > B
' ≥ B. Since
¬D j ∈ I and l(D j ) = l(A), we obtain that (WSii) must hold, and, by the
minimality of l(A), we infer that (WSiib) must hold and that no clause with
head D j contains negated atoms. So, l(D j+1 ) = l(D j ) = l(A) holds by (WSiib)
and the minimality of l(A). Furthermore, the assumption D j+1 ∈ I can be
rejected by the same argument as for A above; otherwise, D j+1 ← would be
the only clause with head D j+1 by minimality of l(D j+1 ) = l(A), contradicting
B < D j+1 . This concludes the inductive proof.
Summarizing, we obtain that D k refers negatively to B
' and that ¬D k ∈ I.
But then there is a clause satisfying (WSii) with head D k and ¬B
' in its body,
and this contradicts the minimality of l(D k ) = l(A). This concludes the proof
of statement (a).
(b) Assume that L(P ) is not definite. Then there exists a clause A ← body
in L(P ) with a negated literal ¬B occurring in body. But then B < A, and
since the bottom stratum consists of minimal components only, we also have
A < B, that is, A and B are in the same component, contradicting (a).
'
(c) First, note that in forming the reduct P of P with respect to ∅, the
third step is the only one in the process which has any effect in that it removes
all non-unit clauses whose heads appear also as heads of unit clauses. Now
'
let A ∈ I be an atom with A ∈ N , and assume without loss of generality
that A is chosen such that l(A) is minimal with these properties. By the first
'
observation and the hypothesis that P satisfies (WS) with respect to I and
l, there must be a clause A ← L 1 , . . . , L n in P such that, for all i, L i is true
with respect to I, and hence true with respect to I
' , and l(A) > l(L i ). Hence,
all the literals L i are true with respect to N by minimality of l(A). Thus,