Herbrand Universe
المؤلف:
Chang, C.-L. and Lee, R. C.-T
المصدر:
Symbolic Logic and Mechanical Theorem Proving. New York: Academic Press, 1997.
الجزء والصفحة:
...
24-1-2022
1434
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.
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.
الاكثر قراءة في المنطق
اخر الاخبار
اخبار العتبة العباسية المقدسة
