57
The Semantics of Logic Programs
Given a normal logic program P and I ∈ I P,4 , we say that U ⊆ B P is
an unfounded set (of P ) with respect to I if each atom A ∈ U satisfies the
following condition. For each clause A ← body in ground(P ) at least one of
the following holds.
(US1) Some (positive or negative) literal in body is false in I.
(US2) Some (non-negated) atom in body occurs in U .
2.6.2 Proposition Let P be a program, and let I ∈ I P,4 . Then there exists
a greatest unfounded set of P with respect to I.
Proof: If (U i ) i∈I is a family of sets, each of which is an unfounded set of P
with respect to I, then it is easy to see that
U i is also an unfounded set
i∈I
of P with respect to I.
•
'
Let P be a program, and recall the definition of the operator T from
P
'
Section 2.4. It is straightforward to lift T to an operator on I P,4 , namely, by
P
'
defining T (I), for I ∈ I P,4 , to be the set of all A ∈ B P for which there is a
P
clause A ← body in ground(P ) with body true in I with respect to Kleene’s
strong three-valued logic. For all I ∈ I P,4 , define U P (I) to be the greatest
unfounded set (of P ) with respect to I. Finally, define
14
'
W P (I) = T (I) ∪ ¬U P (I)
P
for all I ∈ I P,4 . We call W P the W P -operator.
We note that W P does not restrict to a function on I P,3 , which necessitates
using I P,4 instead.
'
2.6.3 Example Consider Program 2.3.1 and I = {p} ∈ I P,3 . Then T (I) =
P
{p} and U P (I) = {p}, so W P (I) = {p, ¬p} ∈ I P,3 .
2.6.4 Proposition Let P be a program. Then W P is monotonic on I P,4 .
'
'
Proof: Let I, K ∈ I P,4 with I ⊆ K. Then we obtain T (I) ⊆ T (K) as in
P
P
the proof of Proposition 2.4.4. So it suffices to show that every unfounded set
of P with respect to I is also an unfounded set of P with respect to K, and
this fact follows immediately from the definition.
•
Since W P is monotonic, it has a least fixed point by the Knaster-Tarski
theorem, Theorem 1.1.10. The least fixed point of W P is called the wellfounded model for P , giving the well-founded semantics of P . We will show
shortly that the well-founded model is always in I P,3 , but let us remark first
that the operator W P is not order continuous in general nor even ω-continuous,
as the following example shows.
14 The operator W P and the well-founded semantics are due to Van Gelder, Ross, and
Schlipf, see [Van Gelder et al., 1991]. However, in the original definition, the operator W P
was not introduced using FOU R.
The Semantics of Logic Programs
Given a normal logic program P and I ∈ I P,4 , we say that U ⊆ B P is
an unfounded set (of P ) with respect to I if each atom A ∈ U satisfies the
following condition. For each clause A ← body in ground(P ) at least one of
the following holds.
(US1) Some (positive or negative) literal in body is false in I.
(US2) Some (non-negated) atom in body occurs in U .
2.6.2 Proposition Let P be a program, and let I ∈ I P,4 . Then there exists
a greatest unfounded set of P with respect to I.
Proof: If (U i ) i∈I is a family of sets, each of which is an unfounded set of P
with respect to I, then it is easy to see that
U i is also an unfounded set
i∈I
of P with respect to I.
•
'
Let P be a program, and recall the definition of the operator T from
P
'
Section 2.4. It is straightforward to lift T to an operator on I P,4 , namely, by
P
'
defining T (I), for I ∈ I P,4 , to be the set of all A ∈ B P for which there is a
P
clause A ← body in ground(P ) with body true in I with respect to Kleene’s
strong three-valued logic. For all I ∈ I P,4 , define U P (I) to be the greatest
unfounded set (of P ) with respect to I. Finally, define
14
'
W P (I) = T (I) ∪ ¬U P (I)
P
for all I ∈ I P,4 . We call W P the W P -operator.
We note that W P does not restrict to a function on I P,3 , which necessitates
using I P,4 instead.
'
2.6.3 Example Consider Program 2.3.1 and I = {p} ∈ I P,3 . Then T (I) =
P
{p} and U P (I) = {p}, so W P (I) = {p, ¬p} ∈ I P,3 .
2.6.4 Proposition Let P be a program. Then W P is monotonic on I P,4 .
'
'
Proof: Let I, K ∈ I P,4 with I ⊆ K. Then we obtain T (I) ⊆ T (K) as in
P
P
the proof of Proposition 2.4.4. So it suffices to show that every unfounded set
of P with respect to I is also an unfounded set of P with respect to K, and
this fact follows immediately from the definition.
•
Since W P is monotonic, it has a least fixed point by the Knaster-Tarski
theorem, Theorem 1.1.10. The least fixed point of W P is called the wellfounded model for P , giving the well-founded semantics of P . We will show
shortly that the well-founded model is always in I P,3 , but let us remark first
that the operator W P is not order continuous in general nor even ω-continuous,
as the following example shows.
14 The operator W P and the well-founded semantics are due to Van Gelder, Ross, and
Schlipf, see [Van Gelder et al., 1991]. However, in the original definition, the operator W P
was not introduced using FOU R.