Herbrands's Theorem

Herbrand's Theorem

Automated theorem proving has two goals: (1) to prove theorems and (2) to do it automatically. Fully automated theorem provers for first-order logic have been developed, starting in the 1960's, but as theorems get more complicated, the time that theorem provers spend tends to grow exponentially. As a result, no really interesting theorems of mathematics can be proved this way- the human life span is not long enough.

Therefore a major problem is to prove interesting theorems and the solution is to give the theorem provers heuristics, rules of thumb for knowledge and wisdom. Some heuristics are fairly general, for example, in a proof that is about t break into several cases do as much as possible that will be of broad applicability before the division into cases occurs. But many heuristics are area-specific; for instance, heuristics appropriate for plane geometry will probably not be appropriate for group theory. The development of good heuristics is a major area of research and requires much experience and insight.

Brief History

In 1930 Kurt Godel and Jaques Herbrand proved the first version of what is now the completeness of predicate calculus. Godel and Herbrand both demonstrated that the proof machinery of the predicate calculus can provide a formal proof for every logically true proposition, while also giving a constructive method for finding the proof, given the proposition.

In 1936 Alonzo Church and Alain Turing independently discovered a fundamental negative property of the predicate calculus. "Until then, there had been an intense search for a positive solution to what was called the decision problem - which was to create an algorithm for the predicate calculus which would correctly determine, for any formal sentence B and any set A of formal sentences, whether or not B is a logical consequence of A. Church and Turing found that despite the existence of the proof procedure, which correctly recognizes (by constructing the proof of B from A) all cases where B is in fact a logical consequence of A, there is not and cannot be an algorithm which can similarly correctly recognize all cases in which B is not a logical consequence of A. "It means that it is pointless to try to program a computer to answer 'yes' or 'no' correctly to every question of the form 'is this a logically true sentence ?'"

Church and Turing proved that it was impossible to find a general decision to verify the inconsistency of a formula. However, there are proof procedures that will verify that a formula is valid if the formula is in fact valid. For invalid formulas, these general procedures will never terminate .

The most significant to automated theorem proving occurred in the 1930's and 1960's. In 1930, Herbrand proved an important theorem that changed the idea of a mechanical theorem prover into a more practicable one. He developed an algorithm to find an interpretation that can falsify a given formula. Since, a valid formula is one that is true under all interpretations, this interpretation cannot exist if the formula is indeed valid, and his algorithm will halt after trying out a finite amount of interpretations. However, it was impossible to implement the refutation procedure which Herbrand's theorem led to because going through the procedure by hand would take forever.

In 1960, Paul Gilmore implemented Herbrand's procedure for the first time on a computer. Later on, however, Martin Davis and Putnam followed with a more efficient procedure. However, the most important breakthrough, during the 60's, in the automated theorem proving world occurred when Robinson reviewed a paper by Davis and Putnam, proposing a predicate-calculus proof procedure that seemed better than Gilmore's, but they still had onto turned it into a practical computer program. Robinson then used programming skills to implement Davis and Putnam's procedure on the Argonne IBM 704. Robinson quickly found that their procedure remained very inefficient. However, while implementing a different procedure also suggested in 1960 by Dag Prawitz, Robinson came to see how the two sets of ideas could be combined into a new, far more efficient, automated proof procedure for first-order predicate logic: ``resolution.``

Herbrand's Theorem

Herbrand's theorem dealt with clauses and literals. A set of clauses (for example {~P(x) v R(x), Q(x) v R(x)}) is unsatisfiable if and only if it is false under all interpretations over all domains (by definition). However, it is impossible to consider all the interpretations over all the domains. This is the importance of Herbrand's contribution. He developed a special domain H such that a set of clauses S is unsatisfiable if and only if S is false under all the interpretations over this domain. This Herbrand universe of S is defined as follows

Let Ho be the set of constants appearing in S. If no constant appears in S, then H0 is to consist of a single constant, say Ho = {a}. For i = 0, 1, 2,..., let Hi+1 be the union of Hi and the set of all terms of the form f^n(t1, .... tn) for all n-place functions f^n occurring

in S, where tj, j= 1, ..., n, are members of the set Hi. Then each Hi is called the i-level constant set of S, and H is called the Herbrand universe of S.

Example:

Let S = {P(a), P(x) v ~P(f(x))}. Then

Ho = {a}

H1 = {a, f(a)}

H2 = {a, f(a), f(f(a))}

.....

H = {a, f(a), f(f(a)), f(f(f(a))), ...}

Herbrand's Theorem:

A set S of clauses is unsatisfiable if and only if there is a finite unsatisfiable set S' of ground instances (A ground instance of a clause C of a set S of clauses obtained by replacing variables in C by members of the Herbrand universe of S) of clauses of S.

The above information basically contains the essence of Herbrand's theorem. I will not discuss Herbrands theorem in detail. Herbrand's contribution opened a world of automated theorem proving that was not possible before. Unlike before where there is an infinite of different domains to test, now the domain is confined by Herbrand's universe. This breakthrough is the basis of Resolution, which made automated theorem proving more effective.

Resolution

Even though Herbrand's procedure was a major breakthrough, it has a major drawback. It requires

...