The Nature of Theorem Proving

Chapter 15 discusses the nature of proof and theorem proving and considers the history of theorem proving from the development of the Logic Theorist theorem prover in 1956. We discuss automated and interactive theorem provers; the nature of mathematical proof and formal mathematical proof; and a selection of existing theorem provers.

1. 1.

   Most existing theorem provers are difficult to use and are for specialist use only. There is a need to improve the usability of theorem provers.

2. 2.

   This position is controversial with others arguing that if correctness is defined mathematically, then the mathematical definition (i.e. formal specification) is a theorem, and the task is to prove that the program satisfies the theorem. They argue that the proofs for non-trivial programs exist and that the reason why there are not many examples of such proofs is due to a lack of mathematical specifications.

3. 3.

   Russell is said to have remarked that he was delighted to see that the Principia Mathematica could be done by machine and that if he and Whitehead had known this in advance that they would not have wasted 10 years doing this work by hand in the early twentieth century.

4. 4.

   Another possibility (though an inefficient and poor simulation of human intelligence) would be to start with the five axioms of the Principia and to apply the three rules of inference to logically derive all possible sequences of valid deductions. This is known as the British Museum algorithm (as sensible as putting monkeys in front of typewriters to reproduce all of the books of the British Museum).

5. 5.

   McCarthy’s viewpoint that predicate logic was the solution for the AI field was disputed by Minsksy and others (resulting in a civil war between the logistics and the proceduralists). The proceduralists argued that formal logic was an inadequate representation of knowledge for AI and that predicate calculus was an overly rigid and inadequate framework. They argued that an alternative approach such as the procedural representation of knowledge was required.

6. 6.

   A formal mathematical proof (of a normal proof) is difficult to write down and can be lengthy. Mathematicians were not really interested in these proof checkers.

Authors and Affiliations

1. SQC Consulting, Mallow, County Cork, Ireland

   Gerard O’Regan

Corresponding author

Correspondence to Gerard O’Regan .

Reprints and permissions

© 2017 Springer International Publishing AG

Policies and ethics