The Nature of Theorem Proving

This chapter discusses the nature of proof and theorem proving, and we discuss automated and interactive theorem provers. We discuss the nature of rigorous mathematical proof and formal mathematical proof.

1. 1.

   Perhaps a good analogy might be that a mathematical proof is like a program written in a high-level language such as C, whereas a formal mathematical proof in logic is like a program written in assembly language.

2. 2.

   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.

3. 3.

   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.

4. 4.

   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.

5. 5.

   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).

6. 6.

   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 logicists 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.

7. 7.

   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. Mallow, Cork, Ireland

   Gerard O’Regan

Reprints and permissions

© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG

Policies and ethics