165
Supported Model Semantics
J(body) = t. The observation that bodies of clauses are finite conjunctions
leads us to conclude the following lemma.
5.4.10 Lemma If T P (I)(A) = t, then T P is locally finite for A and I. Furthermore, T P is continuous at I if and only if it is locally finite for all A with
T P (I)(A) = f .
o
A body C i of a pseudo-clause with head A is false in classical logic if
and only if all the C i are false. Since T P is a Fitting-style operator, we obtain
T P (I)(A) = f if and only if all the C i are false. If we require T P to be locally
finite for A and I, then there must be a finite set S ⊆ B A such that any J ∈ I P
which agrees with I on S renders all the C i false. Conversely, if S ⊆ B A is
a finite set such that any J ∈ I P which agrees with I on S renders all the
C i false, then T is locally finite for A and I. We have just established the
following theorem.
14
5.4.11 Theorem Let P be a normal logic program, and let I ∈ I P . Then
T P is continuous in Q at I if and only if whenever T P (I)(A) = f , then either there is no clause with head A or there exists a finite set S(I, A) =
{A 1 , . . . , A k , B 1 , . . . , B m } ⊆ B P with the following properties.
(a) I(A i ) = t and I(B j ) = f for all i and j.
(b) For every clause A ← body in ground(P ) at least one ¬A i or at least one
B j occurs in body.
In the case of Kleene’s strong three-valued logic, we obtain the following
lemma.
5.4.12 Lemma If Φ P (I)(A) = t, then Φ P is locally finite for A and I. Furthermore, Φ P is continuous if and only if it is locally finite for all A and I
with Φ P (I)(A) ∈ {u, f }.
Similar considerations apply to the Fitting-style operators from Section
5.2.1.
15 We mention in passing that the non-monotonic Gelfond–Lifschitz operator is not a consequence operator in the sense discussed here, and attempts
to characterize the continuity of it involve different methods, some of which
will be studied in Chapter 6.
We will finally provide a generalization of Theorem 5.1.6 for acyclic programs. So let P be acyclic with level mapping l, and let T be a local consequence operator for P . Again, we define the mapping d : I P × I P → R by
d(I, J) = 2
−n , where n is least such that I and J differ on some atom A with
l(A) = n, see Definition 5.1.3 and the remarks following it. It follows from
Propositions 4.3.7 and 5.1.4 that d is a complete ultrametric on I P , a fact
which is easily verified directly.
14 A direct proof without using the notion of local finiteness was given in [Seda, 1995].
15 The operator Ψ P defined by means of Belnap’s four-valued logic, see [Fitting, 2002,
Clifford and Seda, 2000], for example, is also a Fitting-style operator.
Supported Model Semantics
J(body) = t. The observation that bodies of clauses are finite conjunctions
leads us to conclude the following lemma.
5.4.10 Lemma If T P (I)(A) = t, then T P is locally finite for A and I. Furthermore, T P is continuous at I if and only if it is locally finite for all A with
T P (I)(A) = f .
o
A body C i of a pseudo-clause with head A is false in classical logic if
and only if all the C i are false. Since T P is a Fitting-style operator, we obtain
T P (I)(A) = f if and only if all the C i are false. If we require T P to be locally
finite for A and I, then there must be a finite set S ⊆ B A such that any J ∈ I P
which agrees with I on S renders all the C i false. Conversely, if S ⊆ B A is
a finite set such that any J ∈ I P which agrees with I on S renders all the
C i false, then T is locally finite for A and I. We have just established the
following theorem.
14
5.4.11 Theorem Let P be a normal logic program, and let I ∈ I P . Then
T P is continuous in Q at I if and only if whenever T P (I)(A) = f , then either there is no clause with head A or there exists a finite set S(I, A) =
{A 1 , . . . , A k , B 1 , . . . , B m } ⊆ B P with the following properties.
(a) I(A i ) = t and I(B j ) = f for all i and j.
(b) For every clause A ← body in ground(P ) at least one ¬A i or at least one
B j occurs in body.
In the case of Kleene’s strong three-valued logic, we obtain the following
lemma.
5.4.12 Lemma If Φ P (I)(A) = t, then Φ P is locally finite for A and I. Furthermore, Φ P is continuous if and only if it is locally finite for all A and I
with Φ P (I)(A) ∈ {u, f }.
Similar considerations apply to the Fitting-style operators from Section
5.2.1.
15 We mention in passing that the non-monotonic Gelfond–Lifschitz operator is not a consequence operator in the sense discussed here, and attempts
to characterize the continuity of it involve different methods, some of which
will be studied in Chapter 6.
We will finally provide a generalization of Theorem 5.1.6 for acyclic programs. So let P be acyclic with level mapping l, and let T be a local consequence operator for P . Again, we define the mapping d : I P × I P → R by
d(I, J) = 2
−n , where n is least such that I and J differ on some atom A with
l(A) = n, see Definition 5.1.3 and the remarks following it. It follows from
Propositions 4.3.7 and 5.1.4 that d is a complete ultrametric on I P , a fact
which is easily verified directly.
14 A direct proof without using the notion of local finiteness was given in [Seda, 1995].
15 The operator Ψ P defined by means of Belnap’s four-valued logic, see [Fitting, 2002,
Clifford and Seda, 2000], for example, is also a Fitting-style operator.