Herbrand Base and definite programs

Question

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 ?

Answer 1

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.