Resolution theorem proving: a logical point of view

Summary

§1. Introduction. Logical calculi were invented to model mathematical thinking and to formalize mathematical arguments. The calculi of Boole [8] and of Frege [15] can be considered as the first mathematical models of logical inference. Their work paved the way for the discipline of metamathematics, where mathematical reasoning itself is the object of mathematical investigation. The early calculi, the so-called Hilbert type- and Gentzen-type calculi [25], [17] developed in the 20th century served the main purpose to analyze and to reconstruct mathematical proofs and to investigate provability. A practical use of these calculi, i.e., using them for solving actual problems (e.g., for proving theorems in “real” mathematics), was not intended and even did not make sense.

But the idea of a logical calculus as a problem solver is in fact much older than the origin of propositional and predicate logic in the 19th century. Indeed this idea can be traced back toG.W. Leibniz with his brave vision of a calculusratiocinator [29], a calculus which would allow solution of arbitrary problems by purely mechanical computation, once they have been represented in a special formalism. Today we know that, even for restricted languages, this dream of a complete mechanization is not realizable—not even in principle (we just refer to the famous results of Gödel [20] and Turing [39]). That does not imply that we have to reject the idea altogether. Still it makes sense to search for a lean version of the calculus ratiocinator. Concerning the logical language, the ideal candidate is first-order logic; it is axiomatizable (and thus semidecidable), well-understood and sufficiently expressive to represent relevant mathematical structures. By Church's result [10] we know that there is no decision procedure for the validity problem of first-order logic; thus there is no procedure which is 1. capable of verifying the validity of all valid formulas and 2. terminating on all formulas. So, even in first-order logic, we have to be content with the verification of problems. The only thing we can hope for is a calculus which offers a basis for efficient proof search. It is not surprising that the invention of the computer lead to a revival of Leibniz's dream.