Until now we considered arbitrary interpretations of formulae in
predicate logics. In particular we sometimes used numbers as
interpretation domain and functions, like addition or successor. In
the following, we will concentrate on a special case, the Herbrand
interpretation and we will discuss their relation to the general
Let be a set of clauses. The Herbrand universe
for is given by:
- All constants which occur in are in (if no constant appears in , we assume a single constant, say to be in ).
- For every -ary function symbol in and every , .
Examples: Given the clause set , we construct the Herbrand universe
For the clause set we get the Herbrand universe .
Let be a set of clauses. An interpretation
is an Herbrand interpretation iff
- For every -ary function symbol () and
Note, that there is no restriction on the assignments of relations to
predicate symbols (except, that, of course, they have to be
relations over the Herbrand universe ).
In order to discuss the interpretation of predicate symbols, we need
the notion of Herbrand basis.
A ground atom or a ground term is an atom or a
term without an occurrence of a variable.
The Herbrand basis for a set of clauses is the set of
ground atoms , where is a -ary predicate
symbol from and
We will notate the assignments of relations to predicate symbols by
simply giving a set , where each
element is a literal with its atom is from the Herbrand basis.
Let be an interpretation for a set of clauses ; the Herbrand
interpretation corresponding to is a Herbrand
interpretation satisfying the following condition:
Let be Elements from the Herbrand universe
for . By the interpretation every is mapped to a
. If , then have to be assigned in .
Let us now state a simple, very obvious lemma, which will help us,
to focus on Herbrand interpretation in the following.
If is a model for a set of clauses, then every corresponding
Herbrand interpretation is a model for
A set of clauses is unsatisfiable iff there is no Herbrand
model for .
Proof: If is unsatisfiable, there is obviously no Herbrand
model for .
Assume that there is no Herbrand model for and that is
satisfiable. Then, there is a model for and according to
lemma 4 the corresponding Herbrand
interpretation is a model for , which is a