Herbrand base
From Wikipedia, the free encyclopedia
In mathematical logic, for any formal language with a set of terms from the Herbrand universe, the Herbrand base recursively defines the set of all terms that can be composed by applying predicate on the terms from the Herbrand universe.
A Herbrand base of a first-order language L can be constructed from the Herbrand universe of L, by applying to each element of it some predicate from L.
It is thus the set of all ground term atoms which can be constructed using symbols from L.
It is named after Jacques Herbrand.