In first-order logic, a Herbrand structure is a structure over a vocabulary (also sometimes called a signature) 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 is just "" (the symbol). It is named after Jacques Herbrand.
Herbrand structures play an important role in the foundations of logic programming.
The Herbrand universe serves as the universe in a Herbrand structure.
Let , be a first-order language with the vocabulary
then the Herbrand universe of (or of ) is
The relation symbols are not relevant for a Herbrand universe since formulas involving only relations do not correspond to elements of the universe.
A Herbrand structure interprets terms on top of a Herbrand universe.
Let be a structure, with vocabulary and universe . Let be the set of all terms over and be the subset of all variable-free terms. is said to be a Herbrand structure iff
For a constant symbol and a unary function symbol 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 for a Herbrand structure is the set of all atomic formulas whose argument terms are elements of the Herbrand universe.
For a binary relation symbol , we get with the terms from above: