TOPICS
Search

Herbrand Universe


Consider a first-order logic formula Phi in Skolemized form

  forall x_1... forall x_nS.

Then the Herbrand universe H of S is defined by the following rules.

1. All constants from S belong to H. If there are no constants in S, then H contains an arbitrary constant c.

2. If t_1 in H,...,t_n in H, and an n-place function f occurs in S, then f(t_1,...,t_n) in H.

The clauses (disjunctions of literals) obtained from those of S 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 S and terms from H 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.


See also

Unsatisfiable

This entry contributed by Alex Sakharov (author's link)

Explore with Wolfram|Alpha

References

Chang, C.-L. and Lee, R. C.-T. Symbolic Logic and Mechanical Theorem Proving. New York: Academic Press, 1997.Kleene, S. C. Mathematical Logic. New York: Dover, 2002.

Referenced on Wolfram|Alpha

Herbrand Universe

Cite this as:

Sakharov, Alex. "Herbrand Universe." From MathWorld--A Wolfram Web Resource, created by Eric W. Weisstein. https://mathworld.wolfram.com/HerbrandUniverse.html

Subject classifications