Herbrand Semantics

The Herbrand semantics is a semantics for first-order logic. That is, first-order logic gives us symbols we can combine to form sentences; Herbrand semantics gives meaning to those sentences. It's useful for logic programming.

see Herbrand Semantics (Genesereth and Kao)

Herbrand universe

The Herbrand universe for a first-order language L is the set of all ground terms that can be formed in L (notice that relation symbols are irrelevant). It's infinite if L contains any function symbol of arity 1 or greater. e.g. {x,y,f(x),f(y),f(f(x)),…}

Herbrand base

The Herbrand base for a first-order language L is the set of all ground atoms that can be formed in L, that is, using relations from L with arguments from L's Herbrand universe. e.g. {P(x,x),P(x,y),P(y,y),P(y,x),P(f(x),y),…}

Herbrand interpretation

A Herbrand interpretation for a first-order theory T technically includes T's Herbrand universe U, an identity function F, and an arbitrary subset R of T's Herbrand base that is declared to be true. However, R is the only variable part, so that's usually all you need to talk about.
This is a special case of first-order interpretations in which ground terms denote themselves.

Herbrand model

A Herbrand model for a first-order theory T is a Herbrand interpretation of T that is also a model of T.

A Herbrand model is "minimal" if no proper subset of it is also a model.

If there is a single minimal Herbrand model for T, that is called T's least Herbrand model.