27
The Semantics of Logic Programs
preinterpretation J, say, for P , has domain U P and assigns constant and function symbols as follows, where we use the notation of Definition 1.2.7.
(1) For each constant symbol c ∈ L
J
P , c is equal to c.
(2) For each n-ary function symbol f ∈ L , f
J : U
n
P
P → U P is the mapping
defined by f
J (t 1 , . . . , t n ) = f (t 1 , . . . , t n ).
We illustrate these definitions by discussing some of the previous examples
in relation to them. For this purpose, and indeed for all example programs
unless otherwise noted, we consider the Herbrand preinterpretation.
For the program Tweety1 (Program 2.1.2), we obtain
U Tweety1 = {bob, tweety},
B Tweety1 = {penguin(bob), penguin(tweety),
bird(bob), bird(tweety),
flies(bob), flies(tweety)},
and ground(Tweety1) consists of the following clauses.
penguin(tweety) ←
bird(bob) ←
bird(tweety) ← penguin(tweety)
bird(bob) ← penguin(bob)
flies(tweety) ← bird(tweety), ¬penguin(tweety)
flies(bob) ← bird(bob), ¬penguin(bob)
For the successor notation used in the program Even (Program 2.1.3),
the following convention will be convenient: for n ∈ N, we denote the term
s(s(. . . s(x) . . .)), with n occurrences of s, by s
n (x). We then obtain for the
Even program
U Even = {s
n (a) | n
n
∈ N} ,
B Even = {even (s (a)) | n ∈ N} ,
and ground(Even) consists of the following clauses.
even
A
even(a) ←
s
n +1 (a) ← ¬even (s
n (a))
for all n ∈ N
We note that the set ground(Ev
b
en) is infinite. In fact, ground(Even) can
be thought of as an infinite propositional program consisting of clauses p 0 ←
and p n+1 ← ¬p n , where, for each n ∈ N, p n is a propositional variable replacing even (s
n (a)). Often, it is conceptually easier to think of ground(P ) as
a (countably) infinite propositional program and to study it rather than P .