Herbrand theory
From Wikipedia, the free encyclopedia
 |
It has been suggested that this article or section be merged into Herbrand's theorem. (Discuss) |
The Herbrand theory was developed by Jacques Herbrand (1908-1931), a French mathematician. It states that a set of ∀-sentences Φ is unsatisfiable (in first-order sense) if and only if there exists a propositionally unsatisfiable finite set of ground instances Φ0 of Φ.
The Herbrand theory establishes a link between quantification theory and sentential logic. This link is important because it gives a method to test a formula in quantification theory by successively testing formulae for sentential validity. Since testing for sentential validity is a mechanical process, Herbrand's theorem is today of major importance in software developed for automated theorem proving.
 |
This logic-related article is a stub. You can help by expanding it. |
