1,662
edits
Crisperdue (talk  contribs) m (→See also) 
(→Definition: corrected grammar) 

===Definition===
The ''Herbrand universe''
(1) The ''Herbrand universe'' of a firstorder language ''L''<sup>σ</sup>, is the set of all [[Ground_termground terms]] of ''L''<sup>σ</sup>. If the language has no constants, then the language is extended by adding an arbitrary new constant.
*
* In the context of firstorder languages we also speak simply of the ''Herbrand universe'' of the vocabulary σ.
(2) The ''Herbrand universe
* This second definition is important in the context of [[Resolution_(logic)computational resolution]].
