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 atomic formulas that can be composed by forming predicates using 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
 |
This logic-related article is a stub. You can help by expanding it. |
