Herbrand Universe
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.
Contact the MathWorld Team
Bernoulli B(16)