m (→See also)
(→Definition: corrected grammar)
(1) The ''Herbrand universe'' of a first-order language ''L''<sup>σ</sup>, is the set of all [[Ground_term|ground 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 first-order 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]].