43
The Semantics of Logic Programs
Proof: Let I = I
+ ∪ ¬I
− be a three-valued interpretation, and let A ∈
Φ P (I)
+ . Then there is a clause A ← body in ground(P ), where body equals
A 1 , . . . , A n , ¬B 1 , . . . , ¬B k , say, and is true in the three-valued interpretation
I. Therefore, for all i and j, we have A i ∈ I
+ and B j ∈ I
− so that A i ∈ I
+
and B j ∈ I
+ . Therefore, body is true in the two-valued interpretation I
+ , and
so A ∈ T P (I
+ ). Conversely, if I is total, then B j ∈ I
+ means that B j ∈ I
− ,
and hence whenever A ∈ T P (I
+ ) we have A ∈ Φ P (I)
+ . This deals with the
first inclusion.
For the second inclusion, A ∈ Φ P (I)
− if and only if for all clauses A ←
body in ground(P ) we have body false in the three-valued interpretation I.
But then one of the literals in body is false, and so, using the notation already
established for body, either some A i ∈ I
− or some B j ∈ I
+ , that is, either
some A i ∈ I
+ or some B j ∈ I
+ . Therefore, body is also false in the twovalued interpretation I
+ leading to A ∈ T P (I
+ ). We thus obtain Φ P (I)
− ⊆
B P \T P (I
+ ) so that T P (I
+ ) ⊆ B P \Φ P (I)
− . If I is total, then B P \Φ P (I)
− =
'
Φ P (I)
+ = T (I) = T P (I
+ ).
•
P
From Proposition 2.4.13, we immediately obtain that total Fitting models
are always supported. They are, in fact, also stable in general, as we will see
later in Section 2.6. However, if a program has a unique stable model, it does
not necessarily have a total Fitting model.
2.4.14 Program The program consisting of the three clauses
p ← ¬q
q ← ¬p
p ← ¬p
has unique (two-valued) supported model {p}, which is also stable. However,
its (three-valued) Fitting model is everywhere equal to u.
2.5 Perfect Models
The approach using three-valued models, which was presented in Section
2.4, has the advantage that a unique model, namely, the least fixed point of
the Fitting operator, or the Fitting model, can be associated with each given
program. This avoids the ambiguity present in semantics based on classical
logic, such as the stable model semantics, where a program may have many
associated models.
An alternative way of avoiding this problem is to restrict syntax of programs in such a way that only programs are allowed whose semantics is unambiguous. The restriction is usually put in place by conditions which prevent
The Semantics of Logic Programs
Proof: Let I = I
+ ∪ ¬I
− be a three-valued interpretation, and let A ∈
Φ P (I)
+ . Then there is a clause A ← body in ground(P ), where body equals
A 1 , . . . , A n , ¬B 1 , . . . , ¬B k , say, and is true in the three-valued interpretation
I. Therefore, for all i and j, we have A i ∈ I
+ and B j ∈ I
− so that A i ∈ I
+
and B j ∈ I
+ . Therefore, body is true in the two-valued interpretation I
+ , and
so A ∈ T P (I
+ ). Conversely, if I is total, then B j ∈ I
+ means that B j ∈ I
− ,
and hence whenever A ∈ T P (I
+ ) we have A ∈ Φ P (I)
+ . This deals with the
first inclusion.
For the second inclusion, A ∈ Φ P (I)
− if and only if for all clauses A ←
body in ground(P ) we have body false in the three-valued interpretation I.
But then one of the literals in body is false, and so, using the notation already
established for body, either some A i ∈ I
− or some B j ∈ I
+ , that is, either
some A i ∈ I
+ or some B j ∈ I
+ . Therefore, body is also false in the twovalued interpretation I
+ leading to A ∈ T P (I
+ ). We thus obtain Φ P (I)
− ⊆
B P \T P (I
+ ) so that T P (I
+ ) ⊆ B P \Φ P (I)
− . If I is total, then B P \Φ P (I)
− =
'
Φ P (I)
+ = T (I) = T P (I
+ ).
•
P
From Proposition 2.4.13, we immediately obtain that total Fitting models
are always supported. They are, in fact, also stable in general, as we will see
later in Section 2.6. However, if a program has a unique stable model, it does
not necessarily have a total Fitting model.
2.4.14 Program The program consisting of the three clauses
p ← ¬q
q ← ¬p
p ← ¬p
has unique (two-valued) supported model {p}, which is also stable. However,
its (three-valued) Fitting model is everywhere equal to u.
2.5 Perfect Models
The approach using three-valued models, which was presented in Section
2.4, has the advantage that a unique model, namely, the least fixed point of
the Fitting operator, or the Fitting model, can be associated with each given
program. This avoids the ambiguity present in semantics based on classical
logic, such as the stable model semantics, where a program may have many
associated models.
An alternative way of avoiding this problem is to restrict syntax of programs in such a way that only programs are allowed whose semantics is unambiguous. The restriction is usually put in place by conditions which prevent