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.

[edit] See also

In other languages