�
164
Mathematical Aspects of Logic Programming Semantics
other words, we have T (J)(A) = T (I)(A) for each J ∈ B∈S (
/ G B, I(B)),
where S
' = {B 1 , . . . , B k } is a finite set. Since T is local, the value of T (J)(A)
depends only on the values J(A) of atoms
then T (J)(A) = T (I)(A) for all J ∈
is locally finite for A and I. Since A
�
A ∈ B A . So if we set S = S
' ∩ B A ,
B S G(B, I(B)), which is to say that T
∈
was chosen arbitrarily, we obtain that T
is locally finite for I and all A ∈ B P .
•
The following corollary provides a sufficient condition
13 for continuity in
Q.
5.4.8 Corollary Let P be a program, let T be a local consequence operator,
and let l : B P → ω be a level mapping for P with the property that l
−1 (n)
is finite for any n ∈ ω and such that the following property holds: for each
A ∈ B P there exists an n A ∈ ω satisfying l(B) < n A for all B ∈ B A . Then T
is continuous in Q.
Proof: It follows easily from the given conditions that B A is finite for all
A ∈ B P , and hence T is locally finite.
•
We turn now to the study of a particular type of local consequence operator, which we call a Fitting-style operator, and its continuity. Recall from
Section 5.2.1 that bodies of pseudo-clauses may consist of infinite “disjunctions”, but this will not pose any particular difficulties with respect to the
logics we are going to discuss. We note that a program P is of finite type if
and only if all bodies of all pseudo-clauses in P are finite.
Now, if we are given (suitable) truth tables for negation, conjunction, and
disjunction, then we are able to evaluate the truth values of bodies of pseudoclauses relative to given interpretations, as was done in Section 5.2.1.
5.4.9 Definition Let P be a normal logic program. Define the mapping F P :
I P,n → I P,n relative to a given (suitable) logic with n truth values by F P (I) =
J, where J assigns to each A ∈ B P the truth value I( C i ) of the body C i
of the pseudo-clause A
C i with head A.
o
o
o
←
We call operators which satisfy Definition 5.4.9 Fitting-style operators or
the F P -operator. If we impose the mild assumption that t j ← t j evaluates
to true for every j with respect to the underlying logic, then we immediately
obtain that every Fitting-style operator is a local consequence operator. We
will impose this condition, namely, that t j ← t j evaluates to true for every j,
for the remainder of this section.
If the chosen logic is classical two-valued logic, then the corresponding
Fitting-style operator is the immediate consequence operator T P (for a given
program P ). Now, if T P (I)(A) = t, then there exists a clause A ← body in
ground(P ) such that I(body) is true, and we obtain T P (J)(A) = t whenever
13 Communicated to us by Howard A. Blair.
164
Mathematical Aspects of Logic Programming Semantics
other words, we have T (J)(A) = T (I)(A) for each J ∈ B∈S (
/ G B, I(B)),
where S
' = {B 1 , . . . , B k } is a finite set. Since T is local, the value of T (J)(A)
depends only on the values J(A) of atoms
then T (J)(A) = T (I)(A) for all J ∈
is locally finite for A and I. Since A
�
A ∈ B A . So if we set S = S
' ∩ B A ,
B S G(B, I(B)), which is to say that T
∈
was chosen arbitrarily, we obtain that T
is locally finite for I and all A ∈ B P .
•
The following corollary provides a sufficient condition
13 for continuity in
Q.
5.4.8 Corollary Let P be a program, let T be a local consequence operator,
and let l : B P → ω be a level mapping for P with the property that l
−1 (n)
is finite for any n ∈ ω and such that the following property holds: for each
A ∈ B P there exists an n A ∈ ω satisfying l(B) < n A for all B ∈ B A . Then T
is continuous in Q.
Proof: It follows easily from the given conditions that B A is finite for all
A ∈ B P , and hence T is locally finite.
•
We turn now to the study of a particular type of local consequence operator, which we call a Fitting-style operator, and its continuity. Recall from
Section 5.2.1 that bodies of pseudo-clauses may consist of infinite “disjunctions”, but this will not pose any particular difficulties with respect to the
logics we are going to discuss. We note that a program P is of finite type if
and only if all bodies of all pseudo-clauses in P are finite.
Now, if we are given (suitable) truth tables for negation, conjunction, and
disjunction, then we are able to evaluate the truth values of bodies of pseudoclauses relative to given interpretations, as was done in Section 5.2.1.
5.4.9 Definition Let P be a normal logic program. Define the mapping F P :
I P,n → I P,n relative to a given (suitable) logic with n truth values by F P (I) =
J, where J assigns to each A ∈ B P the truth value I( C i ) of the body C i
of the pseudo-clause A
C i with head A.
o
o
o
←
We call operators which satisfy Definition 5.4.9 Fitting-style operators or
the F P -operator. If we impose the mild assumption that t j ← t j evaluates
to true for every j with respect to the underlying logic, then we immediately
obtain that every Fitting-style operator is a local consequence operator. We
will impose this condition, namely, that t j ← t j evaluates to true for every j,
for the remainder of this section.
If the chosen logic is classical two-valued logic, then the corresponding
Fitting-style operator is the immediate consequence operator T P (for a given
program P ). Now, if T P (I)(A) = t, then there exists a clause A ← body in
ground(P ) such that I(body) is true, and we obtain T P (J)(A) = t whenever
13 Communicated to us by Howard A. Blair.