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 (and potentially an arbitrary constant added as a base case, if the language does not contain a constant).
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] See also
[edit] References
 |
This logic-related article is a stub. You can help by expanding it. |
