173
Stable and Perfect Model Semantics
know that some atom from the set S(I, A) must occur in its body. It cannot
occur as any D i because I(D j ) = f for all j. It also cannot occur as any C i
by assumption. So we obtain a contradiction, which finishes the argument.
Conversely, let P be such that the condition on GL P in the statement of
the theorem holds. We will again make use of the observation made at the
beginning of this proof. So let A ∈ B P with GL P (I)(A) = f . If there is no
clause with head A in fix(P ), then there is nothing to show. So assume there
is a clause with head A in fix(P ). Then there is a clause with head A in P , and
by assumption we 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 ground(P )
at least one ¬A i or some B with GL P (I)(B) = f occurs in body. Now let
'
A ← ¬B 1 , . . . , ¬B n be a clause in fix(P ) = T ↑ ω. Then there is k ∈ N with
P
'
A ← ¬B 1 , . . . , ¬B n contained in T ↑ k. Note that n = 0 is impossible since
P
this would imply GL P (I)(A) = t, contradicting the assumption on A. We
proceed by induction on k. If k = 1, then A ← ¬B 1 , . . . , ¬B n is contained
in ground(P ); hence, one of the B j is contained in S(I, A), and this suffices.
For k > 1, there is a clause A ← C 1 , . . . , C m , ¬D 1 , . . . , ¬D m / in ground(P )
'
and clauses C i ← body i in T ↑ (k − 1) which unfold to A ← ¬B 1 , . . . ,
P
¬B n .
By assumption we either have D j ∈ S(I, A) for some j, in which case there
remains nothing to show, or we have that GL P (I)(C i ) = f for some i. In the
latter case we obtain that body i is non-empty by an argument similar to that
of the proof of Proposition 6.2.1. So by assumption there is a (negated) atom
B in body i , and hence B is in {B 1 , . . . , B n }. So again one of the B j is in
S(I, A), and this observation finishes the proof.
•
We also have the following special instance of Theorem 6.2.2.
6.2.3 Corollary Let P be a normal logic program without local variables.
Then GL P is continuous in Q.
Proof: We apply Theorem 6.2.2. Let I ∈ I P and A ∈ B P be such that
GL P (I)(A) = f . Since P has no local variables, it is of finite type. Therefore,
the set B of all negated body atoms in clauses with head A is finite. Let
S(I, A) = {B ∈ B | I(B) = f }; then S(I, A) is also finite. If each clause
with head A contains some negated atom from S(I, A), there is nothing to
prove. So assume that there is a clause A ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m in
ground(P ) with B j ∈ S(I, A) for all j, that is, suppose I(B j ) = t for all j.
Then A ← A 1 , . . . , A n is a clause in P/I and A ∈ T P/I ↑ ω. It now follows that
there is some i with A i ∈ T P/I ↑ ω = GL P (I), and this observation finishes
the argument by Theorem 6.2.2.
•
Measurability is much simpler to deal with, as we see next.
6.2.4 Theorem Let P be a normal logic program. Then GL P is measurable
with respect to σ(Q).
Stable and Perfect Model Semantics
know that some atom from the set S(I, A) must occur in its body. It cannot
occur as any D i because I(D j ) = f for all j. It also cannot occur as any C i
by assumption. So we obtain a contradiction, which finishes the argument.
Conversely, let P be such that the condition on GL P in the statement of
the theorem holds. We will again make use of the observation made at the
beginning of this proof. So let A ∈ B P with GL P (I)(A) = f . If there is no
clause with head A in fix(P ), then there is nothing to show. So assume there
is a clause with head A in fix(P ). Then there is a clause with head A in P , and
by assumption we 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 ground(P )
at least one ¬A i or some B with GL P (I)(B) = f occurs in body. Now let
'
A ← ¬B 1 , . . . , ¬B n be a clause in fix(P ) = T ↑ ω. Then there is k ∈ N with
P
'
A ← ¬B 1 , . . . , ¬B n contained in T ↑ k. Note that n = 0 is impossible since
P
this would imply GL P (I)(A) = t, contradicting the assumption on A. We
proceed by induction on k. If k = 1, then A ← ¬B 1 , . . . , ¬B n is contained
in ground(P ); hence, one of the B j is contained in S(I, A), and this suffices.
For k > 1, there is a clause A ← C 1 , . . . , C m , ¬D 1 , . . . , ¬D m / in ground(P )
'
and clauses C i ← body i in T ↑ (k − 1) which unfold to A ← ¬B 1 , . . . ,
P
¬B n .
By assumption we either have D j ∈ S(I, A) for some j, in which case there
remains nothing to show, or we have that GL P (I)(C i ) = f for some i. In the
latter case we obtain that body i is non-empty by an argument similar to that
of the proof of Proposition 6.2.1. So by assumption there is a (negated) atom
B in body i , and hence B is in {B 1 , . . . , B n }. So again one of the B j is in
S(I, A), and this observation finishes the proof.
•
We also have the following special instance of Theorem 6.2.2.
6.2.3 Corollary Let P be a normal logic program without local variables.
Then GL P is continuous in Q.
Proof: We apply Theorem 6.2.2. Let I ∈ I P and A ∈ B P be such that
GL P (I)(A) = f . Since P has no local variables, it is of finite type. Therefore,
the set B of all negated body atoms in clauses with head A is finite. Let
S(I, A) = {B ∈ B | I(B) = f }; then S(I, A) is also finite. If each clause
with head A contains some negated atom from S(I, A), there is nothing to
prove. So assume that there is a clause A ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m in
ground(P ) with B j ∈ S(I, A) for all j, that is, suppose I(B j ) = t for all j.
Then A ← A 1 , . . . , A n is a clause in P/I and A ∈ T P/I ↑ ω. It now follows that
there is some i with A i ∈ T P/I ↑ ω = GL P (I), and this observation finishes
the argument by Theorem 6.2.2.
•
Measurability is much simpler to deal with, as we see next.
6.2.4 Theorem Let P be a normal logic program. Then GL P is measurable
with respect to σ(Q).