Consider a first-order logic formula 
in Skolemized form
 |
Then the Herbrand universe 
of 
is defined by the following rules.
1. All constants from 
belong to 
.
If there are no constants in 
, then 
contains an arbitrary constant 
.
2. If 
,
and an 
-place
function 
occurs in 
,
then 
.
The clauses (disjunctions of literals) obtained from those of 
by replacing all variables by elements of the Herbrand universe are called ground
clauses, with similar definitions for a ground
literal and ground atom. The set of all ground
atoms that can be formed from predicate symbols from 
and terms from 
is called the Herbrand base.
Consecutive generation of elements of the Herbrand universe and verification of unsatisfiability of generated elements can be straightforwardly implemented in a computer program. Given the completeness of first-order logic, this program is basically a tool for automated theorem proving. Of course, this exhaustive search is too slow for practical applications.
This program will terminate on all unsatisfiable formulas and will not terminate on satisfiable formulas, which basically shows that the set of unsatisfiable formulas is recursively enumerable. Since provability (or equivalently unsatisfiability) in first-order logic is recursively undecidable, this set is not recursive.
