Herbrand Base and definite programs I know the definition of Herbrand Universe and Herbrand Base. But i haven't clearly understood why applying the herbrand base to a definite program leads to a model.
The fact is that an herbrand base doesn't carry information about the predicate symbols that populate the base, so how can i know if the elements of herbrand base are true or false ?
 A: Let $S$ be a formula in clausal where $P_1, \ldots, P_k$ are the
predicate symbols, $f_1,\ldots, f_l$ the function symbols and $a_1, \ldots, a_m$ the constant symbols occurring in $S$.
Let $H_S$ be the Herbrand universe for $S$, i.e. the set of ground terms that can be formed from constants and function symbols in $S$.
Let $B_S$, the Herbrand base for $S$, the set of ground atomic formulas that can be formed from predicate symbols in $S$ and terms in $H_S$.
Consider a simple example: 

$S = \{ \{ ¬P(a,f (x, y)) \}, \{ P(b,f (x, y)) \} \}$.

We have that:

$H_S = \{ a, b, f (a, a), f (a, b), f (b, a), f (b, b), f (a,f (a, a)),\ldots \}$

and:

$B_S = \{ P(a,f (a, a)), P(a,f (a, b)), P(a,f (b, a)), P(a,f (b, b)), \ldots,
P(a, f (a, f (a, a))), \ldots, P(b, f (a, a)), P(b, f (a, b)), P(b, f (b, a)), P(b, f (b, b)), \ldots, P(b, f (a, f (a, a))), \ldots \}$.

To get an Herbrand interpretation for $S$ we have to carve out from $B_S$ the subset corresponding to a relation $R_P$ that interpret the predicate symbol $P$, for example:

$R_P = \{ P(b,f (a, a)), P(b,f (a, b)), P(b,f (b, a)), P(b,f (b, b)) \}$.


Maybe useful to note two facts:


*

*in the case that $S$ has no constants, we add some constant, say $a$, to form ground terms;

*if function symbols are present, the Herbrand universe will be infinite.
