38
Mathematical Aspects of Logic Programming Semantics
Notice that, for any three-valued interpretation I, we have A ∈ Φ P (I)
whenever A is the head of a ground clause and ¬A ∈ Φ P (I) whenever there
is no ground clause whose head is A.
2.4.1 Example We illustrate the calculation of Φ P (I), taking P to be the
program Tweety1 and starting with the three-valued interpretation I = ∅
thought of as a signed subset; of course, ∅ gives truth value u to all ground
atoms in our present context.
We have
'
T (∅) = {penguin(tweety), bird(bob)}
P
and
¬F P (∅) = ¬{penguin(bob)}.
Therefore,
Φ P (∅) = {penguin(tweety), bird(bob), ¬penguin(bob)}.
Continuing, we have
'
T (Φ P (∅)) = {penguin(tweety), bird(bob), bird(tweety), flies(bob)},
P
and
¬F P (Φ P (∅)) = ¬{penguin(bob), flies(tweety)}.
'
Thus, Φ P (Φ P (∅)) = T (Φ P (∅)) ∪ ¬F P (Φ P (∅)) is a total three-valued interpreP
tation. It follows from this fact and Proposition 2.4.4 below that Φ P (Φ P (∅))
is, in fact, the least fixed point of Φ P , as can readily be checked in any case
by iterating Φ P once more.
The development of the operator Φ P somewhat parallels that of T P except
that there are two orderings involved, and the following result is analogous to
Proposition 2.2.2.
2.4.2 Proposition Let P be a normal logic program. Then the three-valued
models for P are exactly the pre-fixed points of Φ P in the truth ordering [ t .
Proof: Suppose that M is a three-valued interpretation for P satisfying
Φ P (M ) [ t M , and let A ∈ B P be arbitrary. Suppose that Φ P (M )(A) = u.
Then we must have M (A) equal to u or to t. Since no clause A ← body
in ground(P ) can have M (body) = t, otherwise Φ P (M )(A) would be equal
to t, we must have M (body) equal to u or to f for each clause A ← body
in ground(P ). But then, on recalling the truth value given to ← in Definition 1.3.3, we see that A ← body is true in M . The other possible values for
Φ P (M )(A) are handled similarly, and so M is a model for P .
The converse is also handled similarly, and we omit the details.
•
Précédent

- 69/305

Suivant