Computational logic: its origins and applications

Lawrence Paulson

Computer Laboratory, University of Cambridge, Cambridge CB3 0FD, UK

e-mail: ku.ca.mac@51pl

An invited Perspective to mark the election of the author to the fellowship of the Royal Society in 2017.

Computer Laboratory, University of Cambridge, Cambridge CB3 0FD, UK

An invited Perspective to mark the election of the author to the fellowship of the Royal Society in 2017.

Received 2017 Dec 13; Accepted 2018 Jan 31.

Abstract

Computational logic is the use of computers to establish facts in a logical formalism. Originating in nineteenth century attempts to understand the nature of mathematical reasoning, the subject now comprises a wide variety of formalisms, techniques and technologies. One strand of work follows the ‘logic for computable functions (LCF) approach’ pioneered by Robin Milner, where proofs can be constructed interactively or with the help of users’ code (which does not compromise correctness). A refinement of LCF, called Isabelle, retains these advantages while providing flexibility in the choice of logical formalism and much stronger automation. The main application of these techniques has been to prove the correctness of hardware and software systems, but increasingly researchers have been applying them to mathematics itself.

Keywords: formal verification, theorem proving, proof assistants, Isabelle, logic for computable functions

Abstract

Acknowledgements

Angeliki Koutsoukou-Argyraki commented on a draft of this paper. The referees also made insightful comments. I would also like to thank Mike Gordon FRS and Robin Milner FRS for their mentorship.

Acknowledgements

Footnotes

^{Thus, a form of the axiom of choice is actually provable in this system [}14, p. 516].

^{Interactive theorem provers are also called}proof assistants.

^{ML can also refer to machine learning.}

^{Mathematical proofs also introduce temporary quantities, as when we allow}x to denote a root of some polynomial. Therefore, contexts may include a string of bound variables, but the details [32] are too complicated to present here.

^Ahomotopy between two continuous functions f and g is a continuous ‘deformation’ of f into g. With this concept one can define an equivalence relation on topological spaces, and the resulting equivalence classes are called homotopy types.

Footnotes

References

1. Woollaston V. 2017. WannaCry ransomware: what is it and how to protect yourself. See .[PubMed]
2. Nicely TR. 2011. Pentium FDIV flaw. See .[PubMed]
3. Lowe G. 1996. Some new attacks upon security protocols. In Proc. 9th Computer Security Foundations Workshop, pp. 162–169. Silver Spring, MD: IEEE Computer Society Press.
4. Boolos GS. 1998. Gottlob Frege and the foundations of arithmetic. In Logic, logic, and logic (ed. GS Boolos), pp. 143–154. Cambridge, MA: Harvard University Press.
5. Gödel K. 1983. Russell’s mathematical logic. In Philosophy of mathematics: selected readings (eds P Benacerraf, H Putnam), 2nd edn, pp. 447–469. Cambridge, UK: Cambridge University Press.
6. Whitehead AN, Russell B. 1962. Principia mathematica. Cambridge, UK: Cambridge University Press; Paperback edition to *56, abridged from the 2nd edition (1927). [PubMed]
7. Boolos GS. 1998. The iterative conception of set. In Logic, logic, and logic (ed. GS Boolos), pp. 13–29. Cambridge, MA: Harvard University Press.
8. Kunen K. 1980 Set theory: an introduction to independence proofs. Amsterdam, The Netherlands: North-Holland. [PubMed]
9. Church A. 1940 A formulation of the simple theory of types. J. Symb. Logic5, 56–68. () [PubMed]
10. Heyting A. 1983. The intuitionist foundations of mathematics. In Philosophy of mathematics: selected readings (eds P Benacerraf, H Putnam), 2nd edn, pp. 52–61. Cambridge, UK: Cambridge University Press.
11. Gödel K. 1995. Some basic theorems on the foundations of mathematics and their implications. In Kurt Gödel: collected works (ed. S Feferman), vol. III, pp. 304–323. Oxford, UK: Oxford University Press.
12. Coquand T, Huet G. 1988. The calculus of constructions. Inf. Comput.76, 95–120. () [PubMed]
13. Martin-Löf P. 1975. An intuitionistic theory of types: predicative part. In Logic colloquium ’73 (eds H Rose, J Shepherdson). Studies in Logic and the Foundations of Mathematics, no. 80, pp. 73–118. Amsterdam, The Netherlands: North-Holland.
14. Martin-Löf P. 1984 Constructive mathematics and computer programming. Phil. Trans. R. Soc. Lond. A312, 501–518. () [PubMed]
15. Wadler P. 2015 Propositions as types. Commun. ACM58, 75–84. () [PubMed]
16. Huth M, Ryan M. 2004. Logic in computer science: modelling and reasoning about systems, 2nd edn Cambridge, UK: Cambridge University Press. [PubMed]
17. Jhala R, Majumdar R. 2009. Software model checking. ACM Comput. Surv.41, 21:1–21:54. () [PubMed]
18. Mathias ARD. 2002 A term of length 4 523 659 424 929. Synthese133, 75–86. () [PubMed]
19. Heule MJH, Kullmann O. 2017. The science of brute force. Commun. ACM60, 70–79. () [PubMed]
20. McCune W. 1997 Solution of the Robbins problem. J. Autom. Reasoning19, 263–276. () [PubMed]
21. Davis M, Putnam H. 1960. A computing procedure for quantification theory. J. ACM7, 207–215. () [PubMed]
22. Robinson JA. 1965 A machine-oriented logic based on the resolution principle. J. ACM12, 23–41. () [PubMed]
23. Turing AM. 1936 On computable numbers, with an application to the Entscheidungsproblem. Proc. Lond. Math. Soc.2, 230–265. () [PubMed]
24. Gordon MJC, Milner R, Wadsworth CP. 1979. Edinburgh LCF: a mechanised logic of computation. Lecture Notes in Computer Science, no. 78. Berlin, Germany: Springer.
25. Gordon MJC, Melham TF. 1993. Introduction to HOL: a theorem proving environment for higher order logic. Cambridge, UK: Cambridge University Press. [PubMed]
26. Harrison J. 1996. HOL Light: a tutorial introduction. In Formal methods in computer-aided design: FMCAD ’96 (eds MK Srivas, AJ Camilleri). Lecture Notes in Computer Science, vol. 1166, pp. 265–269. Berlin, Germany: Springer.
27. Gordon MJC. 1986. Why higher-order logic is a good formalism for specifying and verifying hardware. In Formal aspects of VLSI design (eds G Milne, PA Subrahmanyam), pp. 153–177. Amsterdam, The Netherlands: North-Holland.
28. Harrison J. 2000 Floating point verification in HOL Light: the exponential function. Form. Methods. Syst. Des.16, 271–305. () [PubMed]
29. Bertot Y, Castéran P. 2004. Interactive theorem proving and program development. Coq’Art: the calculus of inductive constructions. Berlin, Germany: Springer. [PubMed]
30. Leroy X. 2006. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In POPL ’06: Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New York, NY, USA, pp. 42–54. New York, NY: ACM Press.
31. Gonthier G. et al. 2013. A machine-checked proof of the odd order theorem. In Interactive theorem proving (eds S Blazy, C Paulin-Mohring, D Pichardie). Lecture Notes in Computer Science, vol. 7998, pp. 163–179. Berlin, Germany: Springer.
32. Paulson LC. 1989 The foundation of a generic theorem prover. J. Autom. Reasoning5, 363–397. () [PubMed]
33. Gordon MJC. 2015 Tactics for mechanized reasoning: a commentary on Milner (1984) ‘the use of machines to assist in rigorous proof’. Phil. Trans. R. Soc. A373, 20140234 () [PubMed]
34. Paulson LC. 1986 Natural deduction as higher-order resolution. J. Logic Program.3, 237–258. () [PubMed]
35. Paulson LC. 1990. Isabelle: the next 700 theorem provers. In Logic and computer science (ed. P Odifreddi), pp. 361–386. New York, NY: Academic Press.
36. Harper R, Honsell F, Plotkin G. 1993. A framework for defining logics. J. ACM40, 143–184. () [PubMed]
37. de Bruijn NG. 1980. A survey of the project AUTOMATH. In To H.B. Curry: essays in combinatory logic, lambda calculus and formalism (eds J Seldin, J Hindley), pp. 579–606. New York, NY: Academic Press.
38. Paulson LC. 1999 A generic tableau prover and its integration with Isabelle. J. Univers. Comput. Sci.5, 73–87. () [PubMed]
39. Paulson LC, Blanchette JC. 2010. Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In Proc. 8th Int. Workshop on the Implementation of Logics, IWIL 2010, Yogyakarta, Indonesia, 9 October, 2011 (eds G Sutcliffe, S Schulz, E Ternovska). EPiC Series in Computing, vol. 2, pp. 1–11. Manchester, UK: EasyChair.
40. Paulson LC. 1999 Inductive analysis of the Internet protocol TLS. ACM Trans. Inf. Syst. Secur.2, 332–351. () [PubMed]
41. Klein G. 2010 sel4: formal verification of an operating-system kernel. Commun. ACM53, 107–115. () [PubMed]
42. Avigad J, Hölzl J, Serafin L. 2017. A formally verified proof of the central limit theorem. J. Autom. Reasoning59, 389–423. () [PubMed]
43. Paulson LC. 2014 A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets. Rev. Symb. Log.7, 484–498. () [PubMed]
44. Paulson LC. 2003 The relative consistency of the axiom of choice—mechanized using Isabelle/ZF. LMS J. Comput. Math.6, 198–248. See ()
45. Wenzel M. 2007 Isabelle/Isar—a generic framework for human-readable proof documents. Stud. Log. Gramm. Rhetor.10, 277–297. [PubMed]
46. Wenzel M. 1997. Type classes and overloading in higher-order logic. In Theorem proving in higher order logics: TPHOLs ’97 (eds EL Gunter, A Felty). Lecture Notes in Computer Science, vol. 1275, pp. 307–322. Berlin, Germany: Springer.
47. Blanchette JC, Nipkow T. 2010. Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In Interactive theorem proving (eds M Kaufmann, LC Paulson). Lecture Notes in Computer Science, vol. 6172, pp. 131–146. Berlin, Germany: Springer.
48. Jutting L. 1977. Checking Landau’s ‘Grundlagen’ in the AUTOMATH System. PhD thesis, Eindhoven University of Technology, Eindhoven, The Netherlands.
49. Rudnicki P, Schwarzweller C, Trybulec A. 2001. Commutative algebra in the Mizar system. J. Symb. Comput.32, 143–169. () [PubMed]
50. Hurd J. 2002 Verification of the Miller-Rabin probabilistic primality test. J. Logic Algebr. Program.56, 3–21. () [PubMed]
51. Hölzl J. 2017 Markov chains and Markov decision processes in Isabelle/HOL. J. Autom. Reasoning59, 345–387. () [PubMed]
52. Boldo S, Joldes M, Muller J, Popescu V. 2017. Formal verification of a floating-point expansion renormalization algorithm. In Proc. of Interactive Theorem Proving—8th Int. Conf., ITP 2017, Brasília, Brazil, 26–29 September 2017 (eds M Ayala-Rincón, CA Muñoz), pp. 98–113. Berlin, Germany: Springer International Publishing.
53. Harrison J. 2007 Formalizing basic complex analysis. Stud. Log. Gramm. Rhetor.10, 151–165. [PubMed]
54. Harrison J. 2009 Formalizing an analytic proof of the prime number theorem. J. Autom. Reasoning43, 243–261. () [PubMed]
55. Hales TC.1998. An overview of the Kepler conjecture. (. )[PubMed]
56. Hales TC.et al.2015A formal proof of the Kepler conjecture. ()[PubMed]
57. Hales TC, Harrison J, McLaughlin S, Nipkow T, Obua S, Zumkeller R. 2010. A revision of the proof of the Kepler conjecture. Discrete Comput. Geom.44, 1–34. () [PubMed]
58. Nipkow T, Bauer G, Schultz P. 2006. Flyspeck I: tame graphs. In Proc. of Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, 17–20 August 2006 (eds U Furbach, N Shankar). Lecture Notes in Artificial Intelligence, vol. 4130, pp. 21–35. Berlin, Germany: Springer.
59. Gonthier G. 2008. The four colour theorem: engineering of a formal proof. In Computer mathematics (ed. D Kapur). Lecture Notes in Computer Sscience, vol. 5081, pp. 333–333. Berlin, Germany: Springer.
60. Fleuriot JD. 2001 A combination of geometry theorem proving and nonstandard analysis, with application to Newton’s Principia. Berlin, Germany: Springer. [PubMed]
61. Lakatos I. 1976 Proofs and refutations: the logic of mathematical discovery. Cambridge, UK: Cambridge University Press. [PubMed]
62. Rota G-C. 2009 Indiscrete thoughts. Berlin, Germany: Springer. [PubMed]
63. Voevodsky V. 2014. The origins and motivations of univalent foundations. In The Institute Letter, pp. 8–9. Princeton, NJ: Institute for Advanced Study. See .[PubMed]
64. The Univalent Foundations Program. 2013. Homotopy type theory: univalent foundations of mathematics. See .[PubMed]
65. Paulson LC, Grabczewski K. 1996. Mechanizing set theory: cardinal arithmetic and the axiom of choice. J. Autom. Reasoning17, 291–323. () [PubMed]
66. Zhan B. 2017. Formalization of the fundamental group in untyped set theory using Auto2. In Proc. of Interactive Theorem Proving—8th Int. Conf., ITP 2017, Brasília, Brazil, 26–29 September 2017 (eds M Ayala-Rincón, CA Muñoz), pp. 514–530. Berlin, Germany: Springer International Publishing.
67. Boolos GS. 1998 Must we believe in set theory? In Logic, logic, and logic (ed. GS Boolos), pp. 120–132. Cambridge, MA: Harvard University Press.
68. MacLane S. 1971 Categories for the working mathematician. Berlin, Germany: Springer. [PubMed]
69. Eberl M. 2017. Semi-automatic asymptotics in Isabelle/HOL. See .[PubMed]
70. Hales TC. 2007 The Jordan curve theorem, formally and informally. Am. Math. Mon.114, 882–894. () [PubMed]
71. Boldo S, Lelay C, Melquiond G. 2015. Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci.9, 41–62. () [PubMed]
72. Kumar R, Myreen MO, Norrish M, Owens S. 2014. CakeML: a verified implementation of ML. In Proc. ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, pp. 179–191. New York, NY: ACM.
73. Avigad J, Harrison J. 2014. Formally verified mathematics. Commun. ACM57, 66–75. () [PubMed]
74. Geuvers H. 2009 Proof assistants: history, ideas and future. Sadhana34, 3–25. () [PubMed]
75. Harrison J, Urban J, Wiedijk F. 2014. History of interactive theorem proving. In Handbook of the history of logic (computational logic) (ed. J Siekmann), vol. 9, pp. 135–214. Amsterdam, The Netherlands: Elsevier.