172
Mathematical Aspects of Logic Programming Semantics
6.2.1 Proposition Let P be a definite logic program, let A ∈ B P , and let
'
n ∈ N. Then A ∈ T P ↑ n if and only if A ← is a clause in T ↑ n.
P
Proof: Let A ∈ T P ↑ n for some n ∈ N. We proceed by induction on n. If
n = 1, then there is nothing to show. So assume that n > 1. Then there is a
clause A ← body in ground(P ) such that all atoms B i in body are contained
in T P ↑ (n − 1), and by the induction hypothesis there are clauses B i ← in
'
T ↑ (n − 1). Unfolding these clauses with A ← body shows that A ← is also
P
'
contained in T P ↑ n.
'
Conversely, assume there is a clause A ← in T ↑ n. We proceed again by
P
induction. If n = 1, there is nothing to show. So let n > 1. Then there exists
'
a clause A ← A 1 , . . . , A k in ground(P ) and clauses A i ← in T ↑ (n − 1). By
P
the induction hypothesis, we obtain A i ∈ T P ↑ (n − 1) for all i, and hence
A ∈ T P ↑ n.
•
Given a program P , we know by Theorem 6.1.4 that GL P is continuous
at some I ∈ I P in Q if and only if T fix(P ) is continuous at I. This gives rise to
the following theorem.
6.2.2 Theorem Let P be a normal logic program, and let I ∈ I P . Then
GL P is continuous at I in Q if and only if whenever GL P (I)(A) = f , then
either there is no clause with head A in ground(P ) or there exists a finite set
S(I, A) = {A 1 , . . . , A k } ⊆ B P such that I(A i ) = t for all i and for every clause
A ← body in ground(P ) at least one ¬A i or some B with GL P (I)(B) = f
occurs in body.
Proof: By Theorem 5.4.11 and Theorem 6.1.4, and by observing that there
are no positive body atoms occuring in fix(P ), we obtain the following.
GL P is continuous at I if and only if whenever GL P (I)(A) = f ,
then either there exists no clause with head A in fix(P ) or
there exists a finite set S(I, A) = {A 1 , . . . , A k } ⊆ B P such
that I(A i ) = t for all i and for every clause A ← body in
fix(P ) at least one ¬A i occurs in body.
So let P be such that GL P is continuous at I. If there is no clause with
head A in ground(P ), then there is nothing to show. So assume that there
is a clause with head A in ground(P ). Then we already know that there
exists a finite set S(I, A) = {A 1 , . . . , A k } ⊆ B P such that I(A i ) = t for
all i and for every clause A ← body in fix(P ) at least one ¬A i occurs in
body. Now let A ← B 1 , . . . , B k , ¬C 1 , . . . , ¬C m be a clause in ground(P ),
and assume that no ¬A i occurs in its body. We show that there is some
B i in body with GL P (I)(B i ) = f . Assume the contrary, that is, that
GL P (I)(B i ) = t for all i. Then for each B i we have B i ∈ GL P (I) = T P/I ↑ ω.
As in the proof of Proposition 6.2.1, we conclude that there is a clause
A ← ¬D 1 , . . . , ¬D n , ¬C 1 , . . . , ¬C m in fix(P ) with D j ∈ I for all j = 1, . . . , n.
Since the clause A ← ¬D 1 , . . . , ¬D n , ¬C 1 , . . . , ¬C m is contained in fix(P ), we
Mathematical Aspects of Logic Programming Semantics
6.2.1 Proposition Let P be a definite logic program, let A ∈ B P , and let
'
n ∈ N. Then A ∈ T P ↑ n if and only if A ← is a clause in T ↑ n.
P
Proof: Let A ∈ T P ↑ n for some n ∈ N. We proceed by induction on n. If
n = 1, then there is nothing to show. So assume that n > 1. Then there is a
clause A ← body in ground(P ) such that all atoms B i in body are contained
in T P ↑ (n − 1), and by the induction hypothesis there are clauses B i ← in
'
T ↑ (n − 1). Unfolding these clauses with A ← body shows that A ← is also
P
'
contained in T P ↑ n.
'
Conversely, assume there is a clause A ← in T ↑ n. We proceed again by
P
induction. If n = 1, there is nothing to show. So let n > 1. Then there exists
'
a clause A ← A 1 , . . . , A k in ground(P ) and clauses A i ← in T ↑ (n − 1). By
P
the induction hypothesis, we obtain A i ∈ T P ↑ (n − 1) for all i, and hence
A ∈ T P ↑ n.
•
Given a program P , we know by Theorem 6.1.4 that GL P is continuous
at some I ∈ I P in Q if and only if T fix(P ) is continuous at I. This gives rise to
the following theorem.
6.2.2 Theorem Let P be a normal logic program, and let I ∈ I P . Then
GL P is continuous at I in Q if and only if whenever GL P (I)(A) = f , then
either there is no clause with head A in ground(P ) or there exists a finite set
S(I, A) = {A 1 , . . . , A k } ⊆ B P such that I(A i ) = t for all i and for every clause
A ← body in ground(P ) at least one ¬A i or some B with GL P (I)(B) = f
occurs in body.
Proof: By Theorem 5.4.11 and Theorem 6.1.4, and by observing that there
are no positive body atoms occuring in fix(P ), we obtain the following.
GL P is continuous at I if and only if whenever GL P (I)(A) = f ,
then either there exists no clause with head A in fix(P ) or
there exists a finite set S(I, A) = {A 1 , . . . , A k } ⊆ B P such
that I(A i ) = t for all i and for every clause A ← body in
fix(P ) at least one ¬A i occurs in body.
So let P be such that GL P is continuous at I. If there is no clause with
head A in ground(P ), then there is nothing to show. So assume that there
is a clause with head A in ground(P ). Then we already know that there
exists a finite set S(I, A) = {A 1 , . . . , A k } ⊆ B P such that I(A i ) = t for
all i and for every clause A ← body in fix(P ) at least one ¬A i occurs in
body. Now let A ← B 1 , . . . , B k , ¬C 1 , . . . , ¬C m be a clause in ground(P ),
and assume that no ¬A i occurs in its body. We show that there is some
B i in body with GL P (I)(B i ) = f . Assume the contrary, that is, that
GL P (I)(B i ) = t for all i. Then for each B i we have B i ∈ GL P (I) = T P/I ↑ ω.
As in the proof of Proposition 6.2.1, we conclude that there is a clause
A ← ¬D 1 , . . . , ¬D n , ¬C 1 , . . . , ¬C m in fix(P ) with D j ∈ I for all j = 1, . . . , n.
Since the clause A ← ¬D 1 , . . . , ¬D n , ¬C 1 , . . . , ¬C m is contained in fix(P ), we