Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 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.
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.
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 the lack of mathematical specifications.
- 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.
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.
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.
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.
References
Boyer R, Moore JS (1979) A computational logic. The Boyer Moore Theorem Prover. Academic Press
MacKensie D (1995) The automation of proof. A historical and sociological exploration. IEEE Ann History Comput 17(3)
Russell B, Whitehead AN (1910) Principia mathematica. Cambridge University Press, Cambridge
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this chapter
Cite this chapter
O’Regan, G. (2020). The Nature of Theorem Proving. In: Mathematics in Computing. Undergraduate Topics in Computer Science. Springer, Cham. https://doi.org/10.1007/978-3-030-34209-8_18
Download citation
DOI: https://doi.org/10.1007/978-3-030-34209-8_18
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-34208-1
Online ISBN: 978-3-030-34209-8
eBook Packages: Computer ScienceComputer Science (R0)