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.
New to topics? Read the docs here!