Herbrand universe
From Wikipedia, the free encyclopedia
In mathematical logic, for any formal language with a set of symbols (constants and functional symbols), the Herbrand universe recursively defines the set of all terms that can be composed by applying functional composition from the basic symbols.
It is named after Jacques Herbrand.
Given a first-order language L, its Herbrand Universe is defined as the set of all ground terms which can be constructed from the symbols of L.
By remembering the definition of ground term, we obtain that the symbols occurring in a Herbrand Universe are the functors and constants from L.
[edit] External links
[edit] See also
 |
This mathematical logic-related article is a stub. You can help Wikipedia by expanding it. |
