31
The Semantics of Logic Programs
systems based on resolution.
6 Thus, in summary, the least model semantics is
very satisfactory for definite logic programs from all points of view.
Attempts to generalize Theorem 2.2.3 to normal programs, however, fail
in several ways, as we show next.
2.2.4 Program Let P be the normal logic program consisting of the following
clauses.
p ← ¬q
q ← ¬p
r ← ¬r
Then {p, r} and {q, r} are minimal, but incomparable, models so that P has
no least model, T P has no fixed points at all (and hence P has no supported
models, see Proposition 2.2.6), and, since T P (∅) = {p, q, r} and T P ({p, q, r}) =
∅, we see that T P is not monotonic.
It is not entirely clear how to cope with the negative results presented by
Program 2.2.4. Various different methods have been discussed in the literature,
leading to different declarative semantics with varying degrees of success. We
will discuss the more prominent of these approaches in the remainder of this
chapter.
A rather straightforward attack is to study minimal models instead of least
models. However, consider the program Even (Program 2.1.3) with models
A
b
K 1 = even s
2n (a) | n ∈ N
and
A
b
2n+1 (a)
K 2 = even s
| n ∈ N .
Both models are minimal, but it seems to be rather obvious that K 1 captures
the intended meaning of Even, while K 2 does not. Essentially, this arises from
the fact that even(s(a)) is true with respect to K 2 , although the program
itself gives no justification for this. Thus, it would seem intuitively reasonable
that whenever an atom is true in an intended model for a program P , then
it should be true for a reason provided by the program itself. This idea is
captured by the following definition, see [Apt et al., 1988].
2.2.5 Definition An interpretation I for a program P is called supported if
for each A ∈ I there is a clause A ← body in ground(P ) with I(body) = t.
Continuing the Even program discussion above, note that K 1 is supported,
whereas K 2 is not. Indeed, K 1 is the only supported model for Even, as we
will see later. So, for some programs, supportedness is an appropriate requirement of models. Supportedness is also captured by the immediate consequence
operator, as follows.
6 A detailed account of resolution-based logic programming can be found in [Apt, 1997,
Lloyd, 1987].
The Semantics of Logic Programs
systems based on resolution.
6 Thus, in summary, the least model semantics is
very satisfactory for definite logic programs from all points of view.
Attempts to generalize Theorem 2.2.3 to normal programs, however, fail
in several ways, as we show next.
2.2.4 Program Let P be the normal logic program consisting of the following
clauses.
p ← ¬q
q ← ¬p
r ← ¬r
Then {p, r} and {q, r} are minimal, but incomparable, models so that P has
no least model, T P has no fixed points at all (and hence P has no supported
models, see Proposition 2.2.6), and, since T P (∅) = {p, q, r} and T P ({p, q, r}) =
∅, we see that T P is not monotonic.
It is not entirely clear how to cope with the negative results presented by
Program 2.2.4. Various different methods have been discussed in the literature,
leading to different declarative semantics with varying degrees of success. We
will discuss the more prominent of these approaches in the remainder of this
chapter.
A rather straightforward attack is to study minimal models instead of least
models. However, consider the program Even (Program 2.1.3) with models
A
b
K 1 = even s
2n (a) | n ∈ N
and
A
b
2n+1 (a)
K 2 = even s
| n ∈ N .
Both models are minimal, but it seems to be rather obvious that K 1 captures
the intended meaning of Even, while K 2 does not. Essentially, this arises from
the fact that even(s(a)) is true with respect to K 2 , although the program
itself gives no justification for this. Thus, it would seem intuitively reasonable
that whenever an atom is true in an intended model for a program P , then
it should be true for a reason provided by the program itself. This idea is
captured by the following definition, see [Apt et al., 1988].
2.2.5 Definition An interpretation I for a program P is called supported if
for each A ∈ I there is a clause A ← body in ground(P ) with I(body) = t.
Continuing the Even program discussion above, note that K 1 is supported,
whereas K 2 is not. Indeed, K 1 is the only supported model for Even, as we
will see later. So, for some programs, supportedness is an appropriate requirement of models. Supportedness is also captured by the immediate consequence
operator, as follows.
6 A detailed account of resolution-based logic programming can be found in [Apt, 1997,
Lloyd, 1987].