In first-order logic, a Herbrand structure S is a structure over a vocabulary σ that is defined solely by the syntactical properties of σ. The idea is to take the symbol strings of terms as their values, e.g. the denotation of a constant symbol c is just "c" (the symbol). It is named after Jacques Herbrand.
Herbrand structures play an important role in the foundations of logic programming.[1]
The Herbrand universe serves as the universe in the Herbrand structure.
Let, be a first-order language with the vocabulary
then the Herbrand universe of (or) is .
Notice that the relation symbols are not relevant for a Herbrand universe.
A Herbrand structure interprets terms on top of a Herbrand universe.
Let S be a structure, with vocabulary σ and universe U. Let W be the set of all terms over σ and W0 be the subset of all variable-free terms. S is said to be a Herbrand structure iff
For a constant symbol c and a unary function symbol f(.) we have the following interpretation:
In addition to the universe, defined in, and the term denotations, defined in, the Herbrand base completes the interpretation by denoting the relation symbols.
A Herbrand base is the set of all ground atoms whose argument terms are elements of the Herbrand universe.
For a binary relation symbol R, we get with the terms from above: