= Herbrand structure
{c}
= Herbrand interpretation
{c}
{synonym}
A <first-order structure> whose domain is the <Herbrand universe>, with constants denoting themselves and function symbols acting by syntactic term formation. Its predicates are specified by assigning <truth values> to ground atoms. With <first-order equality>, ordinary equality of syntactic terms imposes additional restrictions; more general term models may require quotienting by a congruence.
Equivalently, the predicate meanings of a <Herbrand interpretation> correspond to a subset of its <Herbrand base>.
Back to article page
