Elamur Research⌕
☰
home / papers / 2014 / History of Interactive Theorem Proving

History of Interactive Theorem Proving

Paper · 2014 · John Harrison, Josef Urban and Freek Wiedijk

Summary

This book chapter traces the history of formal proof built through human–machine cooperation, as opposed to proving done entirely by the computer. The authors argue that fully automated provers began to level off after early breakthroughs such as unification. Human-guided proving has therefore become the realistic path for formalizing non-trivial mathematics and for verifying hardware and software.

The chapter offers no new data or experiments. It is a historical survey that begins with early efforts: Abrahams' Proofchecker (1963), Bledsoe's attempt to formalize Morse's set theory, and the SAM family. It then follows the major lineages of systems: Automath and its type-theoretic descendants (Coq, NuPRL, LF), LCF and the HOL family, Mizar, NQTHM, PVS and others.

A thematic part covers recurring ideas:

  • procedural versus declarative proof languages,
  • reliability through small trusted kernels,
  • reflection,
  • integration with automated tools,
  • machine learning for premise selection.

Its main contribution is an organized overview of a field that lacked one, showing where the central ideas of today's provers came from.

Key points

  • SAM V was used in 1966 to settle a previously unproven lattice-theory conjecture, now known as "SAM's Lemma."
  • Automath was the first system to encode proofs via the Curry-Howard isomorphism. The chapter distinguishes two variants: formulas represented as types (Coq, Agda, NuPRL), and formulas paired with a type of proof objects (LF, Automath).
  • Mizar still checks complete proof scripts in batch mode. Its Mizar Mathematical Library (MML) is a long-running formalization effort.
  • The authors note that automated proving has been centered mainly in the USA, while interactive proving has been centered in Europe. They also see the two approaches now converging, for example through SMT and hammer tools such as Sledgehammer.
  • Large formalizations discussed include Flyspeck (Kepler conjecture), the Feit-Thompson theorem and the Prime Number Theorem.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputer Science Applications · 184 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as John Harrison, Josef Urban and Freek Wiedijk. 2014. History of Interactive Theorem Proving. Handbook of the History of Logic, vol. 9 (Elsevier).

The paper itself, not this page. BibTeX from the library's record of the work.

@article{harrison2014history,
  title = {{History of Interactive Theorem Proving}},
  author = {John Harrison, Josef Urban and Freek Wiedijk},
  journal = {Handbook of the History of Logic, vol. 9 (Elsevier)},
  year = {2014},
  doi = {10.1016/b978-0-444-51624-4.50004-6},
  url = {https://doi.org/10.1016/b978-0-444-51624-4.50004-6}
}

References

363 references, 6 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Ralph Back. Correctness Preserving Program Transformations: Proof Theory and Applications, volume 131 of Mathematical Centre Tracts. Mathematical Centre, Amsterdam, 1980. find
  2. Antonia Balaa and Yves Bertot. Fix-point equations for well-founded recursion in type theory. In Aagaard and Harrison [2000], pages 1–16. find
  3. Grzegorz Bancerek and Piotr Rudnicki. A compendium of continuous lattices in Mizar. J. Autom. Reasoning, 29(3-4):189–224, 2002. find
  4. Grzegorz Bancerek and Piotr Rudnicki. Information retrieval in MML. In MKM, volume 2594 of Lecture Notes in Computer Science, pages 119–132. Springer, 2003. find
  5. Grzegorz Bancerek. Information retrieval and rendering with MML Query. In Jonathan M. Borwein and William M. Farmer, editors, MKM, volume 4108 of Lecture Notes in Computer Science, pages 266–279. Springer, 2006. find
  6. H. P. Barendregt. Lambda calculi with types. In S. Abramsky, Dov M. Gabbay, and S. E. Maibaum, editors, Handbook of Logic in Computer Science (Vol. 2), pages 117–309. Oxford University Press, 1992. find
  7. Henk Barendregt. The impact of the lambda calculus on logic and computer science. Bulletin of Symbolic Logic, 3:181–215, 1997. find
  8. Bruno Barras and Benjamin Werner. Coq in Coq. Unpublished report, available at www.lix.polytechnique.fr/~barras/publi/coqincoq.pdf, 1996. find
  9. H. Barringer, J. Cheng, and C. B. Jones. A logic covering undefinedness in program proofs. Acta Informatica, 21:251–269, 1984. find
  10. Joseph L. Bates and Robert L. Constable. Proofs as programs. ACM Transactions on Programming Languages and Systems, 7:113–136, 1985. find
  11. Bernhard Beckert and Joachim Posegga. leanTAP : Lean, tableau-based deduction. Journal of Automated Reasoning, 15:339–358, 1995. find
  12. M. J. Beeson. Foundations of constructive mathematics: metamathematical studies, volume 3 of Ergebnisse der Mathematik und ihrer Grenzgebiete. Springer-Verlag, 1984. find
  13. Stefan Berghofer and Markus Wenzel. Inductive datatypes in HOL — lessons learned in formal-logic engineering. In Bertot et al. [1999], pages 19–36. find
  14. J. A. Bergstra, Y. Hirshfield, and J. V. Tucker. Meadows and the equational specification of division. Theoretical Computer Science, 410:1261–1271, 2007. find
  15. Yves Bertot and Laurent Théry. A generic approach to building user interfaces for theorem provers. J. Symb. Comput., 25(2):161–194, 1998. find
  16. Yves Bertot, Gilles Kahn, and Laurent Théry. Proof by pointing. In Masami Hagiya and John C. Mitchell, editors, TACS, volume 789 of Lecture Notes in Computer Science, pages 141–160. Springer, 1994. find
  17. Yves Bertot, Gilles Dowek, André Hirschowitz, Christine Paulin, and Laurent Théry, editors. Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs’99, volume 1690 of Lecture Notes in Computer Science, Nice, France, 1999. Springer-Verlag. find
  18. Norman L. Biggs, E. Keith Lloyd, and Robin J. Wilson. Graph Theory 1736–1936. Clarendon Press, 1976. find
  19. Graham Birtwistle and P. A. Subrahmanyam, editors. Current Trends in Hardware Verification and Automated Theorem Proving. Springer-Verlag, 1989. find
  20. Errett Bishop and Douglas Bridges. Constructive analysis, volume 279 of Grundlehren der mathematischen Wissenschaften. Springer-Verlag, 1985. find
  21. Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, and Nicholas Smallbone. Encoding monomorphic and polymorphic types. In Nir Piterman and Scott A. Smolka, editors, TACAS, volume 7795 of Lecture Notes in Computer Science, pages 493–507. Springer, 2013. find
  22. J. C. Blanchette, J. Hölzl, A. Lochbihler, L. Panny, A. Popescu, and D. Traytel. Truly modular (co)datatypes for Isabelle/HOL. In Klein and Gamboa [2014], pages 93–110. find
  23. W. W. Bledsoe and Peter Bruell. A man-machine theorem-proving system. Artificial Intelligence, 5:51–72, 1974. John Harrison, Josef Urban and Freek Wiedijk find
  24. W. W. Bledsoe and E. J. Gilbert. Automatic theorem proof-checking in set theory: A preliminary report. Technical Report SC-RR-67-525, Sandia National Lab, 1967. find
  25. W. W. Bledsoe. Some automatic proofs in analysis. In W. W. Bledsoe and D. W. Loveland, editors, Automated Theorem Proving: After 25 Years, volume 29 of Contemporary Mathematics, pages 89–118. American Mathematical Society, 1984. find
  26. Manuel Blum. Program result checking: A new approach to making programs more reliable. In Andrzej Lingas, Rolf Karlsson, and Svante Carlsson, editors, Automata, Languages and Programming, 20th International Colloquium, ICALP93, Proceedings, volume 700 of Lecture Notes in Computer Science, pages 1–14… find
  27. Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. A formally-verified C compiler supporting floating-point arithmetic. In Alberto Nannarelli, Peter-Michael Siedel, and Ping Tak Peter Tang, editors, 21st IEEE symposium on computer arithmetic, ARITH 21, proceedings, pages 107… find
  28. Richard Boulton, Andrew Gordon, Mike Gordon, John Harrison, John Herbert, and John Van Tassel. Experience with embedding hardware description languages in HOL. In Victoria Stavridou, Thomas F. Melham, and R. T. Boute, editors, Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem… find
  29. Richard Boulton. Boyer-Moore automation for the HOL system. In Claesen and Gordon [1992], pages 133–142. find
  30. Richard John Boulton. Efficiency in a fully-expansive theorem prover. Technical Report 337, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK, 1993. Author’s PhD thesis. find
  31. Nicolas Bourbaki. Theory of sets. Elements of mathematics. Addison-Wesley, 1968. Translated from French ‘Théorie des ensembles’ in the series ‘Eléments de mathématique’, originally published by Hermann in 1968. find
  32. Ana Bove, Peter Dybjer, and Ulf Norell. A Brief Overview of Agda - A Functional Language with Dependent Types. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, Augus… find
  33. Robert S. Boyer and J Strother Moore. A Computational Logic. ACM Monograph Series. Academic Press, 1979. find
  34. Robert S. Boyer and J Strother Moore. Metafunctions: proving them correct and using them efficiently as new proof procedures. In Robert S. Boyer and J Strother Moore, editors, The Correctness Problem in Computer Science, pages 103–184. Academic Press, 1981. find
  35. Robert S. Boyer and J Strother Moore. A Computational Logic Handbook, volume 23 of Perspectives in Computing. Academic Press, 1988. find
  36. James P. Bridge, Sean B. Holden, and Lawrence C. Paulson. Machine learning for first-order theorem proving. Journal of Automated Reasoning, pages 1–32, 2014. find
  37. Randall E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35:677–691, 1986. find
  38. Bruno Buchberger. Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. PhD thesis, Mathematisches Institut der Universität Innsbruck, 1965. English translation in Journal of Symbolic Computation vol. 41 (2006), pp. 475–511. find
  39. R. Bumcrot. On lattice complements. Proceedings of the Glasgow Mathematical Association, 7:22–23, 1965. find
  40. A. Bundy, F. van Harmelen, J. Hesketh, and A. Smaill. Experiments with proof plans for induction. Journal of Automated Reasoning, 7:303–323, 1991. find
  41. Alan Bundy, editor. 12th International Conference on Automated Deduction, volume 814 of Lecture Notes in Computer Science, Nancy, France, 1994. Springer-Verlag. find
  42. J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 10 20 states and beyond. Information and Computation, 98:142– 170, 1992. History of Interactive Theorem Proving find
  43. R. M. Burstall. Proving properties of programs by structural induction. The Computer Journal, 12:41–48, 1969. find
  44. Juanito Camilleri and Tom Melham. Reasoning with inductively defined relations in the HOL theorem prover. Technical Report 265, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK, 1992. find
  45. Olga Caprotti and Martin Oostdijk. Formal and efficient primality proofs by the use of computer algebra oracles. Journal of Symbolic Computation, 32:55–70, 2001. find
  46. Rudolf Carnap. The Logical Syntax of Language. International library of psychology, philosophy and scientific method. Routledge & Kegan Paul, 1937. Translated from ‘Logische Syntax der Sprache’ by Amethe Smeaton (Countess von Zeppelin), with some new sections not in the German original. find
  47. Jan Cederquist, Thierry Coquand, and Sara Negri. The Hahn-Banach Theorem in Type Theory. In G. Sambin and J. Smith, editors, Twenty-five years of Constructive Type Theory, pages 57–72, 1998. find
  48. Amine Chaieb and Tobias Nipkow. Proof synthesis and reflection for linear arithmetic. Journal of Automated Reasoning, 41, 2008. find
  49. Wilfred Chen. Tactic-based theorem proving and knowledge-based forward chaining. In Kapur [1992], pages 552–566. find
  50. S.-C. Chou. Mechanical Geometry Theorem Proving. Reidel, 1988. find
  51. Alonzo Church. A formulation of the Simple Theory of Types. Journal of Symbolic Logic, 5:56–68, 1940. find
  52. Luc J. M. Claesen and Michael J. C. Gordon, editors. Proceedings of the IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and its Applications, volume A-20 of IFIP Transactions A: Computer Science and Technology, IMEC, Leuven, Belgium, 1992. North-Holland. find
  53. Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Dextrer Kozen, editor, Logics of Programs, volume 131 of Lecture Notes in Computer Science, pages 52–71, Yorktown Heights, 1981. Springer-Verlag. find
  54. Cyril Cohen and Assia Mahboubi. A formal quantifier elimination for algebraically closed fields. In Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Calculemus, volume 6167 of Lecture Notes in Computer Science, pages 189–203. Springer-Verlag, 2010. find
  55. Robert L. Constable and Joseph L. Bates. The Nearly Ultimate PEARL. Technical Report TR 83-551, Department of Computer Science, Cornell University, January 1983. find
  56. Robert L. Constable and Michael J. O’Donnell. A programming logic, with an introduction to the PL/CV verifier. Winthrop, 1978. find
  57. Robert Constable. Implementing Mathematics with The Nuprl Proof Development System. Prentice-Hall, 1986. find
  58. D. C. Cooper. Theorem proving in arithmetic without multiplication. In B. Melzer and D. Michie, editors, Machine Intelligence 7, pages 91–99. Elsevier, 1972. find
  59. Coq development team. The Coq proof assistant reference manual, 2012. Version 8.4pl4. find
  60. Thierry Coquand and Gérard Huet. The calculus of constructions. Inf. Comput., 76(2/3):95–120, 1988. find
  61. Thierry Coquand and Christine Paulin. Inductively defined types. In Per Martin-Löf and Grigori Mints, editors, COLOG-88, International Conference on Computer Logic, Tallinn, USSR, December 1988, Proceedings, volume 417 of LNCS, pages 50–66. Springer, 1990. find
  62. Catarina Coquand, Dan Synek, and Makoto Takeyama. An Emacs-Interface for Type-Directed Support for Constructing Proofs and Programs. In European Joint Conferences on Theory and Practice of Software, 2005. find
  63. Guy Cousineau and Michel Mauny. The Functional Approach to Programming. Cambridge University Press, 1998. John Harrison, Josef Urban and Freek Wiedijk find
  64. D. Craigen, S. Kromodimeoljo, I. Meisels, B. Pase, and M. Saaltink. EVES: An overview. In S. Prehn and W. J. Toetenel, editors, VDM ’91: Formal Software Development Methods, volume 551 of Lecture Notes in Computer Science, pages 389–405. Springer-Verlag, 1991. find
  65. Paul Curzon. Tracking design changes with formal machine-checked proof. The Computer Journal, 38:91–100, 1995. find
  66. Ingo Dahn and Christoph Wernhard. First order proof problems extracted from an article in the MIZAR mathematical library. In Maria Paola Bonacina and Ulrich Furbach, editors, International Workshop on First-Order Theorem Proving, volume 97-50 of RISC-Linz Report Series, pages 58–62. RISC-Linz, 1997. find
  67. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7:201–215, 1960. find
  68. M. Davis. A computer program for Presburger’s algorithm. In Summaries of talks presented at the Summer Institute for Symbolic Logic, Cornell University, pages 215–233. Institute for Defense Analyses, Princeton, NJ, 1957. Reprinted in Siekmann and Wrightson [1983], pp. 41–48. find
  69. Martin Davis. Obvious logical inferences. In Patrick J. Hayes, editor, IJCAI, pages 530–531. William Kaufmann, 1981. find
  70. Jared Davis. A Self-Verifying Theorem Prover. PhD thesis, University of Texas at Austin, 2009. find
  71. N.G. de Bruijn. AUTOMATH, a language for mathematics. Technical Report 68-WSK-05, Department of Mathematics, Eindhoven University of Technology, November 1968. find
  72. N.G. de Bruijn. The mathematical language AUTOMATH, its usage, and some of its extensions, 1968. find
  73. N.G. de Bruijn. The mathematical language AUTOMATH, its usage, and some of its extensions. In Symposium on Automatic Demonstration, IRIA, Versailles, France, number 125 in LNCS, pages 29–61. Springer, December 1968. Also published in Selected Papers on Automath, Studies in Logic and the Foundations… find
  74. N.G. de Bruijn. SEMIPAL 2, an extension of the mathematical notational language SEMIPAL. Technical Report Notitie 1969/43, Department of Mathematics, Eindhoven University of Technology, March 1969. find
  75. N.G. de Bruijn. A Processor for PAL. Technical Report Notitie 1970/30, Department of Mathematics, Eindhoven University of Technology, March 1970. find
  76. N.G. de Bruijn. Verslag over het project Wiskundige Taal AUTOMATH, September 1978. find
  77. N.G. de Bruijn. Wees contextbewust in WOT. Euclides, (55):7–12, 1979. find
  78. N.G. de Bruijn. Gedachten rondom AUTOMATH, March 1990. find
  79. Philippe de Groote. Defining Lambda-Typed Lambda-Calculi by Axiomatiz-ing the Typing Relation. In Patrice Enjalbert, Alain Finkel, and Klaus W. Wagner, editors, STACS 93, 10th Annual Symposium on Theoretical Aspects of Computer Science, Würzburg, Germany, February 25-27, 1993, Proceedings, volume 6… find
  80. Leonardo de Moura and Grant Passmore. The strategy challenge in SMT solving. In Maria Paola Bonacina and Mark E Stickel, editors, Automated Reasoning and Mathematics: Essays in Memory of William McCune, volume 7788 of Lecture Notes in Computer Science, pages 15–44. Springer-Verlag, 2013. find
  81. David Delahaye. A tactic language for the system Coq. In Michel Parigot and Andrei Voronkov, editors, Logic Programming and Automated Reasoning, LPAR 2000, volume 1955 of Lecture Notes in Computer Science, pages 85–95, La reunion, France, 2000. Springer-Verlag. find
  82. Ewen Denney. A prototype proof translator from HOL to Coq. In Aagaard and Harrison [2000], pages 108–125. find
  83. J. Denzinger and S. Schulz. Recording and Analysing Knowledge-Based Distributed Deduction Processes. Journal of Symbolic Computation, 21(4/5):523–541, 1996. find
  84. Stephanie Dick. The work of proof in the age of human-machine collaboration. Isis, 102:494–505, 2011. History of Interactive Theorem Proving find
  85. E. W. Dijkstra and C. S. Scholten. Predicate Calculus and Program Semantics. Springer-Verlag, 1990. find
  86. E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976. find
  87. Lucas Dixon. A Proof Planning Framework for Isabelle. PhD thesis, University of Edinburgh, 2005. find
  88. Marko Van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk, editors. Interactive Theorem Proving, Second International Conference ITP, volume 6898 of Lecture Notes in Computer Science. Springer-Verlag, 2011. find
  89. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In E. Giunchiglia and A. Tacchella, editors, Theory and Applications of Satisfiability Testing: 6th International Conference SAT 2003, volume 2919 of Lecture Notes in Computer Science, pages 502–518. Springer-Verlag, 2003.
  90. Norbert Eisinger and Hans Jürgen Ohlbach. The Markgraf Karl refutation procedure (MKRP). In Jorg H. Siekmann, editor, 8th International Conference on Automated Deduction, volume 230 of Lecture Notes in Computer Science, pages 681–682, Oxford, England, 1986. Springer-Verlag. find
  91. William Farmer, Joshua Guttman, and Javier Thayer. IMPS: an interactive mathematical proof system. In M. E. Stickel, editor, 10th International Conference on Automated Deduction, volume 449 of Lecture Notes in Computer Science, pages 653–654, Kaiserslautern, Federal Republic of Germany, 1990. Spring… find
  92. Edward A. Feigenbaum and Julian Feldman, editors. Computers & Thought. AAAI Press / MIT Press, 1995. find
  93. A.P. Felty and D. Howe. Hybrid interactive theorem proving using Nuprl and HOL. In William McCune, editor, Automated Deduction — CADE-14, volume 1249 of Lecture Notes in Computer Science, pages 351–365, Townsville, Australia, 1997. Springer-Verlag. find
  94. Frederic Brenton Fitch. Symbolic Logic: an introduction. The Ronald Press Company, New York, 1952. find
  95. Jacques Fleuriot. A Combination of Geometry Theorem Proving and Nonstandard Analysis with Application to Newton’s Principia. Distinguished dissertations. Springer-Verlag, 2001. Revised version of author’s PhD thesis. find
  96. R. W. Floyd. Assigning meanings to programs. In Proceedings of AMS Symposia in Applied Mathematics, 19: Mathematical Aspects of Computer Science, pages 19–32. American Mathematical Society, 1967. find
  97. Ulrich Furbach and Natarajan Shankar, editors. Proceedings of the third International Joint Conference, IJCAR 2006, volume 4130 of Lecture Notes in Computer Science, Seattle, WA, 2006. Springer-Verlag. find
  98. D. Gabbay, I. Hodkinson, and M. Reynolds. Temporal Logic. Oxford University Press, 1994. find
  99. Ruben Gamboa. Mechanically Verifying Real-Valued Algorithms in ACL2. PhD thesis, University of Texas at Austin, 1999. find
  100. Mohan Ganesalingam. The Language of Mathematics: A Linguistic and Philosophical Investigation, volume 7805 of Lecture Notes in Computer Science. Springer-Verlag, 2013. find
  101. H. Gelerntner. Realization of a geometry-theorem proving machine. In Proceedings of the International Conference on Information Processing, UNESCO House, pages 273–282, 1959. Also appears in Siekmann and Wrightson [1983], pp. 99–117 and in Feigenbaum and Feldman [1995], pp. 134–152. find
  102. Herman Geuvers and Erik Barendsen. Some logical and syntactical observations concerning the first-order dependent type system lambda-P. Mathematical Structures in Computer Science, 9(4):335–359, 1999. find
  103. P. C. Gilmore. A proof method for quantification theory: Its justification and realization. IBM Journal of Research and Development, 4:28–35, 1960. find
  104. Fausto Giunchiglia and Alan Smaill. Reflection in constructive and non-constructive automated reasoning. In Harvey Abramson and M. H. Rogers, editors, Meta-Programming in Logic Programming, pages 123–140. MIT Press, 1989. John Harrison, Josef Urban and Freek Wiedijk find
  105. Evgueni Goldberg and Yakov Novikov. BerkMin: a fast and robust Sat-solver. In Carlos Delgado Kloos and Jose Da Franca, editors, Design, Automation and Test in Europe Conference and Exhibition (DATE 2002), pages 142–149, Paris, France, 2002. IEEE Computer Society Press. find
  106. Georges Gonthier and Assia Mahboubi. An introduction to small scale reflection in Coq. Journal of Formalized Reasoning, 3(2):95–152, 2010. find
  107. Georges Gonthier, Assia Mahboubi, and Enrico Tassi. A Small Scale Reflection Extension for the Coq system. Technical Report RR-6455, INRIA, 2008. find
  108. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A machine-checked proof of the odd order theorem. In S.… find
  109. Georges Gonthier. Verifying the safety of a practical concurrent garbage collector. In Rajeev Alur and Thomas A. Henzinger, editors, Proceedings of the 8th international conference on computer aided verification (CAV’96), volume 1102 of Lecture Notes in Computer Science, pages 462–465, New Brunswick… find
  110. Georges Gonthier. A computer-checked proof of the four colour theorem. Available at http://research.microsoft.com/~gonthier/4colproof.pdf, 2005. ↗
  111. Georges Gonthier. Formal proof — the four-color theorem. Notices of the AMS, 35:1382–1393, 2008. find
  112. D. I. Good, R. L. London, and W. W. Bledsoe. An interactive program verification system. IEEE Transactions on Software Engineering, 1:59–67, 1979. find
  113. D. I. Good. Toward a Man-Machine System for Proving Program Correctness. PhD thesis, University of Wisconsin, 1970. find
  114. D. I. Good. Proof of a distributed system in Gypsy. In M. J. Elphick, editor, Formal Specification: Proceedings of the Joint IBM/University of Newcastle upon Tyne Seminar, pages 44–89. University of Newcastle upon Tyne, Computing Laboratory, 1983. find
  115. R. L. Goodstein. Recursive Number Theory. Studies in Logic and the Foundations of Mathematics. North-Holland, 1957. find
  116. Michael J. C. Gordon, Robin Milner, and Christopher P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979. find
  117. Michael J. C. Gordon, James Reynolds, Warren Hunt, and Matt Kaufmann. An integration of HOL and ACL2. In Proceedings of the 6th international conference on Formal Methods in Computer-Aided Design (FMCAD), pages 153–160. IEEE Computer Society Press, 2006. find
  118. Michael J. C. Gordon. Representing a logic in the LCF metalanguage. In D. Néel, editor, Tools and notions for program construction: an advanced course, pages 163– 185. Cambridge University Press, 1982. find
  119. Mike Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. Technical Report 77, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK, 1985. find
  120. M. J. C. Gordon. Mechanizing programming logics in higher order logic. In Birtwistle and Subrahmanyam [1989], pages 387–439. find
  121. M. J. C. Gordon. From LCF to HOL: A short history. In Gordon Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, language, and interaction: essays in honour of Robin Milner. MIT Press, 2000.
  122. Benjamin Grégoire, Laurent Théry, and Benjamin Wener. A computational approach to Pocklington certificates in type theory. In Proceedings of the 8th International Symposium on Functional and Logic Programming, volume 3945 of Lecture Notes in Computer Science, pages 97–113. Springer-Verlag, 2006. find
  123. Timothy Griffin. Efs - an interactive environment for formal systems. In Ewing L. Lusk and Ross A. Overbeek, editors, 9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings, volume 310 of LNCS, pages 740–741. Springer, 1988. History of Interactive T… find
  124. J. R. Guard, F. C. Oglesby, J. H. Bennett, and L. G. Settle. Semi-automated mathematics. Journal of the ACM, 16:49–62, 1969. find
  125. Elsa L. Gunter. A broader class of trees for recursive type definitions for HOL. In Joyce and Seger [1993], pages 141–154. find
  126. Thomas C. Hales, John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua, and Roland Zumkeller. A revision of the proof of the Kepler conjecture. Discrete and Computational Geometry, 44:1–34, 2010. find
  127. Thomas C. Hales. A proof of the Kepler conjecture. Annals of Mathematics, 162:1065–1185, 2005. find
  128. Thomas C. Hales. Introduction to the Flyspeck project. In Thierry Coquand, Henri Lombardi, and Marie-Françoise Roy, editors, Mathematics, Algorithms, Proofs, volume 05021 of Dagstuhl Seminar Proceedings. Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Ger… find
  129. Thomas Hales. Dense Sphere Packings: A Blueprint for Formal Proofs, volume 400 of London Mathematical Society Lecture Note Series. Cambridge University Press, 2012. find
  130. F. K. Hanna and N. Daeche. Specification and verification using higher-order logic: A case study. In G. Milne and P. A. Subrahmanyam, editors, Formal Aspects of VLSI Design: Proceedings of the 1985 Edinburgh Workshop on VLSI, pages 179– 213, 1986. find
  131. Robert Harper, Furio Honsell, and Gordon D. Plotkin. A Framework for Defining Logics. In Proceedings, Symposium on Logic in Computer Science, 22-25 June 1987, Ithaca, New York, USA, pages 194–204. IEEE Computer Society, 1987. find
  132. John Harrison and Laurent Théry. A sceptic’s approach to combining HOL and Maple. Journal of Automated Reasoning, 21:279–294, 1998. find
  133. John Harrison. Inductive definitions: automation and application. In Phillip J. Windley, Thomas Schubert, and Jim Alves-Foss, editors, Higher Order Logic Theorem Proving and Its Applications: Proceedings of the 8th International Workshop, volume 971 of Lecture Notes in Computer Science, pages 200–21… find
  134. John Harrison. Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK, 1995. Available on the Web as http://www.cl.cam.ac.uk/users/jrh/papers/reflect.ps.gz. ↗
  135. John Harrison. HOL Light: A tutorial introduction. In Mandayam Srivas and Albert Camilleri, editors, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD’96), volume 1166 of Lecture Notes in Computer Science, pages 265–269. Springer-Verlag, 1996. find
  136. John Harrison. A Mizar mode for HOL. In Wright et al. [1996], pages 203–220. find
  137. John Harrison. Proof style. In Eduardo Giménez and Christine Paulin-Mohring, editors, Types for Proofs and Programs: International Workshop TYPES’96, volume 1512 of Lecture Notes in Computer Science, pages 154–172, Aussois, France, 1996. Springer-Verlag. find
  138. John Harrison. Theorem Proving with the Real Numbers. Springer-Verlag, 1998. Revised version of author’s PhD thesis. find
  139. John Harrison. Formal verification of floating point trigonometric functions. In Warren A. Hunt and Steven D. Johnson, editors, Formal Methods in Computer-Aided Design: Third International Conference FMCAD 2000, volume 1954 of Lecture Notes in Computer Science, pages 217–233. Springer-Verlag, 2000. find
  140. John Harrison. Complex quantifier elimination in HOL. In Richard J. Boulton and Paul B. Jackson, editors, TPHOLs 2001: Supplemental Proceedings, pages 159– 174. Division of Informatics, University of Edinburgh, 2001. Published as Informatics Report Series EDI-INF-RR-0046. Available on the Web at htt… find
  141. John Harrison. Isolating critical cases for reciprocals using integer factorization. In Jean-Claude Bajard and Michael Schulte, editors, Proceedings, 16th IEEE Symposium on Computer Arithmetic, pages 148–157, Santiago de Compostela, Spain, 2003. IEEE Computer Society. Currently available from sympos… find
  142. John Harrison. The HOL Light tutorial. Unpublished manual available at http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf, 2006. John Harrison, Josef Urban and Freek Wiedijk ↗
  143. John Harrison. Towards self-verification of HOL Light. In Furbach and Shankar [2006], pages 177–191. find
  144. John Harrison. Verifying nonlinear real formulas via sums of squares. In Schneider and Brandt [2007], pages 102–118. find
  145. John Harrison. Formalizing an analytic proof of the Prime Number Theorem (dedicated to Mike Gordon on the occasion of his 60th birthday). Journal of Automated Reasoning, 43:243–261, 2009. find
  146. John Harrison. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009. find
  147. Percy John Heawood. Map-colour theorem. Quarterly Journal of Pure and Applied Mathematics, 24:332–338, 1890. Reprinted in Biggs et al. [1976]. find
  148. Martin C. Henson. Elements of functional languages. Blackwell Scientific, 1987. find
  149. Thomas T. Hewett. ACM SIGCHI curricula for human-computer interaction. Technical report, New York, NY, USA, 1992. find
  150. Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Eli Barzilay, Yegor Bryukhov, Richard Eaton, Adam Granicz, Alexei Kopylov, Christoph Kreitz, Vladimir Krupski, Lori Lorigo, Stephan Schmitt, Carl Witty, and Xin Yu. MetaPRL - A Modular Logical Environment. In David A. Basin and Burk… find
  151. C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12:576–580, 583, 1969. find
  152. Peter V. Homeier. A design structure for higher order quotients. In Joe Hurd and Tom Melham, editors, Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, volume 3603 of Lecture Notes in Computer Science, pages 130– 146, Oxford, UK, 2005. Springer-Verlag. find
  153. Peter V. Homeier. The HOL-Omega logic. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009, volume 5674 of Lecture Notes in Computer Science, pages 244–259, Munich,… find
  154. Douglas J. Howe. Reflecting the semantics of reflected proof. In Peter Aczel, Harold Simmons, and Stanley Wainer, editors, Proof Theory, pages 229–250. Cambridge University Press, 1992. find
  155. Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith, Jörn Richts, and Jörg Siekmann. Omega-MKRP: A proof development environment. In Bundy [1994], pages 788–792. find
  156. Gérard Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975. find
  157. Warren A. Hunt and Sol Swords. Centaur Technology media unit verification. In Ahmed Bouajjani and Oded Maler, editors, CAV ’09: Proceedings of the 21st International Conference on Computer Aided Verification, volume 5643 of Lecture Notes in Computer Science, pages 353–367, Grenoble, France, 2009. Sp… find
  158. W. A. Hunt. FM8501: A Verified Microprocessor. PhD thesis, University of Texas, 1985. Published by Springer-Verlag as volume 795 of the Lecture Notes in Computer Science series, 1994. find
  159. Joe Hurd. Integrating Gandalf and HOL. In Bertot et al. [1999], pages 311–321. find
  160. Joe Hurd. First-order proof tactics in higher-order logic theorem provers. In Workshop on Design and Application of Strategies/Tactics in Higher Order Logics. NASA, 2003. NASA technical report NASA/CP-2003-212448. find
  161. Joe Hurd. The OpenTheory standard theory library. In César Muñoz, editor, Proceedings of the Second NASA Formal Methods Symposium (NFM 2010), number NASA/CP-2010-216215 in Technical Report, pages 177–191, Langley Research Center, Hampton VA 23681-2199, USA, 2010. find
  162. Kenneth E. Iverson. Notation as a tool of thought. Communications of the ACM, 23:444–465, 1980.
  163. S. Jaśkowski. On the rules of supposition in formal logic. Studia Logica, 1:5–32, 1934. find
  164. T. J. Jech. The Axiom of Choice, volume 75 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1973. History of Interactive Theorem Proving find
  165. Kathleen Jensen and Niklaus Wirth. Pascal user manual and report. Springer-Verlag, 1974. find
  166. J. Jeuring, J. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge, editors. Intelligent Computer Mathematics - 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Proje… find
  167. Jeffrey J. Joyce and Carl Seger, editors. Proceedings of the 1993 International Workshop on the HOL theorem proving system and its applications, volume 780 of Lecture Notes in Computer Science, UBC, Vancouver, Canada, 1993. Springer-Verlag. find
  168. Roope Kaivola and Mark D. Aagaard. Divider circuit verification with model checking and theorem proving. In Aagaard and Harrison [2000], pages 338–355. find
  169. Roope Kaivola and Katherine Kohatsu. Proof engineering in the large: Formal verification of the Pentium (R) 4 floating-point divider. In T. Margaria and Tom Melham, editors, 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001, volume 2144 of Lecture Notes in Computer Science, pages 1… find
  170. Cezary Kaliszyk and Alexander Krauss. Scalable LCF-style proof translation. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Proc. of the 4th International Conference on Interactive Theorem Proving (ITP’13), volume 7998 of LNCS, pages 51–66. Springer Verlag, 2013. find
  171. Cezary Kaliszyk and Josef Urban. HOL(y)Hammer: Online ATP service for HOL Light. Mathematics in Computer Science, 2014. http://dx.doi.org/10.1007/s11786-014-0182-0. ↗
  172. Cezary Kaliszyk and Josef Urban. Learning-assisted theorem proving with millions of lemmas. Journal of Symbolic Computation, 2014. In press, http://arxiv.org/abs/1402.3578 . — [arXiv:1402.3578](https://arxiv.org/abs/1402.3578) ↗
  173. Cezary Kaliszyk. Web interfaces for proof assistants. Electr. Notes Theor. Comput. Sci., 174(2):49–61, 2007. find
  174. L. A. Kaluzhnin. On an information language for mathematics. Applied Linguistic and Machine Translation, pages 21–29, 1962. find
  175. Deepak Kapur, editor. 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Computer Science, Saratoga, NY, 1992. Springer-Verlag. find
  176. Matt Kaufmann and Lawrence C. Paulson, editors. First International Conference on Interactive Theorem Proving, ITP 2010, volume 6172 of Lecture Notes in Computer Science, Edinburgh, UK, 2010. Springer-Verlag. find
  177. Matt Kaufmann, Panagiotis Manolios, and J Strother Moore. Computer-Aided Reasoning: ACL2 Case Studies. Kluwer, 2000. find
  178. Matt Kaufmann, Panagiotis Manolios, and J Strother Moore. Computer-Aided Reasoning: An Approach. Kluwer, 2000. find
  179. Chantal Keller and Benjamin Werner. Importing HOL Light into Coq. In Kaufmann and Paulson [2010], pages 307–322. find
  180. Alfred Braye Kempe. On the geographical problem of the four colours. American Journal of Mathematics, 2:193–200, 1879. Reprinted in Biggs et al. [1976]. find
  181. J. C. King. A Program Verifier. PhD thesis, Carnegie-Mellon University, 1969. find
  182. Gerwin Klein and Ruben Gamboa, editors. Fifth International Conference on Interactive Theorem Proving, ITP 2014, volume 8558 of Lecture Notes in Computer Science, Vienna, Austria, 2014. Springer-Verlag. find
  183. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an os kernel. Communications of the ACM, 53:107–115, 2010. find
  184. B. Knaster. Un théorème sur les fonctions d’ensembles. Annales de la Société Polonaise de Mathématique, 6:133–134, 1927. Volume published in 1928. find
  185. T. Knoblock and R. Constable. Formalized metareasoning in type theory. In Proceedings of the First Annual Symposium on Logic in Computer Science, pages 237–248, Cambridge, MA, USA, 1986. IEEE Computer Society Press. John Harrison, Josef Urban and Freek Wiedijk find
  186. Donald Knuth and Peter Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra. Pergamon Press, 1970. find
  187. Dean Blackmar Krafft. AVID: a system for the interactive development of verifiably correct programs. PhD thesis, Department of Computer Science, Cornell University, 1981. find
  188. Alexander Krauss. Partial and nested recursive function definitions in higher-order logic. Journal of Automated Reasoning, 44:303–336, 2010. find
  189. Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, and Tom Heskes. Overview and evaluation of premise selection techniques for large theory mathematics. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, IJCAR, volume 7364 of LNCS, pages 378–392. Springer, 2012. find
  190. Daniel Kühlwein, Stephan Schulz, and Josef Urban. E-MaLeS 1.1. In Maria Paola Bonacina, editor, CADE, volume 7898 of Lecture Notes in Computer Science, pages 407–413. Springer, 2013. find
  191. Ramana Kumar and Tjark Weber. Validating QBF validity in HOL4. In Eekelen et al. [2011], pages 168–183. find
  192. Ramaya Kumar, Thomas Kropf, and Klaus Schneider. Integrating a first-order automatic prover in the HOL environment. In Archer et al. [1991], pages 170–176. find
  193. Ramana Kumar, Rob Arthan, Magnus O. Myreen, and Scott Owens. HOL with definitions: Semantics, soundness and a verified implementation. In Klein and Gamboa [2014], pages 308–324. find
  194. Ondr̆ej Kunc̆ar. Proving valid quantified boolean formulas in HOL Light. In Eekelen et al. [2011], pages 184–199. find
  195. Kenneth Kunen. Nonconstructive computational mathematics. Journal of Automated Reasoning, 21:69–97, 1998. find
  196. Imre Lakatos. Proofs and Refutations: the Logic of Mathematical Discovery. Cambridge University Press, 1976. Edited by John Worrall and Elie Zahar. Derived from Lakatos’s Cambridge PhD thesis; an earlier version was published in the British Journal for the Philosophy of Science vol. 14. find
  197. C. W. H. Lam. How reliable is a computer-based proof? The Mathematical Intelligencer, 12:8–12, 1990. find
  198. Leslie Lamport and P. Michael Melliar-Smith. Synchronizing clocks in the presence of faults. Journal of the ACM, 32:52–78, 1985. find
  199. Peter J. Landin. The next 700 programming languages. Communications of the ACM, 9:157–166, 1966. find
  200. Maurice Lecat. Erreurs de Mathématiciens des origines à nos jours. Ancne Libraire Castaigne et Libraire Ém Desbarax, Brussels, 1935. find
  201. Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107–115, 2009. find
  202. A.A. Letichevsky, A.V. Lyaletski, and M.K. Morokhovets. Glushkovs evidence algorithm. Cybernetics and Systems Analysis, 49(4):489–500, 2013. find
  203. R. L. London. Computer programs can be proved correct. In Proceedings of the IVth Systems Symposium at Cape Western Reserve University. Springer-Verlag, 1970. find
  204. Donald W. Loveland. Mechanical theorem-proving by model elimination. Journal of the ACM, 15:236–251, 1968. find
  205. Donald W. Loveland. Automated theorem proving: a logical basis. North-Holland, 1978. find
  206. Zhaohui Luo. ECC, an Extended Calculus of Constructions. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS ’89), Pacific Grove, California, USA, June 5-8, 1989, pages 386–395. IEEE Computer Society, 1989. find
  207. Zhaohui Luo. A unifying theory of dependent types: The schematic approach. In Anil Nerode and Michael A. Taitslin, editors, Logical Foundations of Computer Science - Tver ’92, Second International Symposium, Tver, Russia, July 20-24, 1992, Proceedings, volume 620 of LNCS, pages 293–304. Springer, 19… find
  208. Zhaohui Luo. PAL + : a lambda-free logical framework. J. Funct. Program., 13(2):317–338, 2003. History of Interactive Theorem Proving find
  209. Alexander V. Lyaletski and Konstantin Verchinine. Evidence algorithm and system for automated deduction: A retrospective view. In Autexier et al. [2010], pages 411–426. find
  210. Saunders Mac Lane. Mathematics: Form and Function. Springer-Verlag, 1986. find
  211. Donald MacKenzie. Mechanizing Proof: Computing, Risk and Trust. MIT Press, 2001. find
  212. Lena Magnusson and Bengt Nordström. The ALF Proof Editor and Its Proof Engine. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs, International Workshop TYPES’93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers, volume 806 of LNCS, pages 213–237. Springer, 199… find
  213. Lionel Mamane and Herman Geuvers. A document-oriented Coq plugin for TeXmacs. In Manuel Kauers, Manfred Kerber, Robert Miner, and Wolfgang Windsteiger, editors, MKM 2007 - Work in Progress, volume 07-06 of RISC Report, pages 47–60. University of Linz, Austria, 2007. find
  214. Leo Marcus, Stephen D. Crocker, and Jalsook R. Landauer. SDVS: A system for verifying microcode correctness. ACM Sigsoft Software Engineering Notes, 10(4):7– 14, 1985. find
  215. Per Martin-Löf. Intuitionistic type theory. Bibliopolis, 1984. find
  216. S. Ju. Maslov. An inverse method of establishing deducibility in classical predicate calculus. Doklady Akademii Nauk, 159:17–20, 1964. find
  217. Roman Matuszewski and Piotr Rudnicki. Mizar: the first 30 years. Mechanized Mathematics and Its Applications, 4:3–24, 2005. find
  218. David A. McAllester. ONTIC: A Knowledge Representation System for Mathematics. MIT Press, 1989. find
  219. John McCarthy. Computer programs for checking mathematical proofs. In Proceedings of the Fifth Symposium in Pure Mathematics of the American Mathematical Society, pages 219–227. American Mathematical Society, 1961. find
  220. W. McCune and R. Padmanabhan. Automated Deduction in Equational Logic and Cubic Curves, volume 1095 of Lecture Notes in Computer Science. Springer-Verlag, 1996. find
  221. W. McCune. Solution of the Robbins problem. Journal of Automated Reasoning, 19:263–276, 1997. find
  222. Sean McLaughlin and John Harrison. A proof-producing decision procedure for real arithmetic. In Robert Nieuwenhuis, editor, CADE-20: 20th International Conference on Automated Deduction, proceedings, volume 3632 of Lecture Notes in Computer Science, pages 295–314, Tallinn, Estonia, 2005. Springer-Ve… find
  223. Sean Mclaughlin, Clark Barrett, and Yeting Ge. Cooperating theorem provers: A case study combining HOL-Light and CVC Lite. In Proceedings of the 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning, volume 144 of Electronic Notes in Theoretical Computer Science, 2005. find
  224. Sean McLaughlin. An interpretation of Isabelle/HOL in HOL Light. In Furbach and Shankar [2006], pages 192–204. find
  225. K. L. McMillan. Interpolation and SAT-based model checking. In Warren A. Hunt and Fabio Somenzi, editors, Computer Aided Verification, 15th International Conference, CAV 2003, volume 2725 of Lecture Notes in Computer Science, pages 1–13, Boulder, CO, 2003. Springer-Verlag. find
  226. Norman D. Megill. Metamath: A computer language for pure mathematics. Unpublished; available on the Web from ftp://ftp.shore.net/members/ndm/metamath.ps.gz., 1996. find
  227. Thomas F. Melham. Automating recursive type definitions in higher order logic. In Birtwistle and Subrahmanyam [1989], pages 341–386. find
  228. Thomas F. Melham. The HOL logic extended with quantification over type variables. In Claesen and Gordon [1992], pages 3–18. find
  229. P. Michael Melliar-Smith and John Rushby. The Enhanced HDM system for specification and verification. ACM Software Engineering Notes, 10(4), 1985. John Harrison, Josef Urban and Freek Wiedijk find
  230. Jia Meng and L. C. Paulson. Translating higher-order problems to first-order clauses. In Geoff Sutcliffe, Renate Schmidt, and Stephan Schulz, editors, ESCoR: Empirically Succesful Computerized Reasoning, 2006. find
  231. Robin Milner. Implementation and applications of Scott’s logic for computable functions. ACM SIGPLAN Notices, 7(1):1–6, January 1972. find
  232. Robin Milner. A theory of type polymorphism in programming. Journal of Computer and Systems Sciences, 17:348–375, 1978. find
  233. J Strother Moore and Claus-Peter Wirth. Automation of mathematical induction as part of the history of logic. Available from http://arxiv.org/abs/1309.6226, 2013. — [arXiv:1309.6226](https://arxiv.org/abs/1309.6226) ↗
  234. J Strother Moore, Tom Lynch, and Matt Kaufmann. A mechanically checked proof of the correctness of the kernel of the AM D5 K 86 floating-point division program. IEEE Transactions on Computers, 47:913–926, 1998. find
  235. Carroll Morgan. Programing from Specifications. Prentice-Hall, 1990. find
  236. A. P. Morse. A theory of sets. Academic Press, 1965. find
  237. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference (DAC 2001), pages 530–535. ACM Press, 2001.
  238. Magnus O. Myreen and Jared Davis. The reflective Milawa theorem prover is sound, down to the machine code that runs it. To appear in ITP 2014, 2014. find
  239. Pavel Naumov, Mark-Oliver Stehr, and José Meseguer. The HOL/NuPRL proof translator (a practical approach to formal interoperability). In Richard J. Boulton and Paul B. Jackson, editors, TPHOLs, volume 2152 of Lecture Notes in Computer Science, pages 329–345. Springer, 2001. find
  240. Adam Naumowicz and Czeslaw Bylinski. Basic elements of computer algebra in MIZAR. Mechanized Mathematics and Its Applications, 2, 2002. find
  241. Adam Naumowicz and Czeslaw Bylinski. Improving Mizar texts with properties and requirements. In Andrea Asperti, Grzegorz Bancerek, and Andrzej Trybulec, editors, MKM, volume 3119 of Lecture Notes in Computer Science, pages 290–301. Springer, 2004. find
  242. Peter Naur. Proof of algorithms by general snapshots. BIT, 6:310–216, 1966. find
  243. George C. Necula and Peter Lee. Proof generation in the Touchstone theorem prover. In David McAllester, editor, Automated Deduction — CADE-17, volume 1831 of Lecture Notes in Computer Science, pages 25–44, Pittsburgh, PA, USA, 2000. Springer-Verlag. find
  244. R. P. Nederpelt, J. H. Geuvers, and R. C. De Vrijer. Selected papers on Automath. Studies in logic and the foundations of mathematics. Elsevier, Amsterdam, 1994. find
  245. Greg Nelson and Derek Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1:245–257, 1979. find
  246. Greg Nelson and Derek Oppen. Fast decision procedures based on congruence closure. Journal of the ACM, 27:356–364, 1980. find
  247. A. Newell and H. A. Simon. The logic theory machine. IRE Transactions on Information Theory, 2:61–79, 1956. find
  248. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL — A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer-Verlag, 2002. find
  249. Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin-Löf ’s Type Theory. Oxford Sciences Publication, Oxford, 1990. find
  250. Steven Obua and Sebastian Skalberg. Importing HOL into Isabelle/HOL. In Furbach and Shankar [2006], pages 298–302. find
  251. John O’Leary, Xudong Zhao, Rob Gerth, and Carl-Johan H. Seger. Formally verifying IEEE compliance of floating-point hardware. Intel Technology Journal, 1999-Q1:1–14, 1999. Available on the Web as http://download.intel.com/technology/itj/q11999/pdf/floating_point.pdf. ↗
  252. John O’Leary, Roope Kaivola, and Tom Melham. Relational STE and theorem proving for formal verification of industrial circuit designs. In Barbara Jobstmann and Sandip Ray, editors, FMCAD 2013: Formal Methods in Computer-Aided Design, pages 97–104. IEEE, 2013. History of Interactive Theorem Proving
  253. S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Kapur [1992], pages 748–752. find
  254. Petros Papapanagiotou. On the automation of inductive proofs in HOL Light. Master’s thesis, University of Edinburgh, 2007. find
  255. Pablo A. Parrilo. Semidefinite programming relaxations for semialgebraic problems. Mathematical Programming, 96:293–320, 2003. find
  256. Hanna Patkowska. A homotopy extension theorem for fundamental sequences. Fundamenta Mathematicae, 64(1):87–89, 1969. find
  257. Wolfgang Paul. Towards a worldwide verification techology. In B. Meyer and J. Woodcock, editors, Verified Software, volume 4171 of Lecture Notes in Computer Science, pages 19–25. Springer-Verlag, 2008. find
  258. Lawrence C. Paulson and Jasmin Christian Blanchette. Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In Geoff Sutcliffe, Eugenia Ternovska, and Stephan Schulz, editors, Proceedings of the 8th International Workshop on the Implementatio… find
  259. Lawrence C. Paulson and Krzysztof Gra̧bczewski. Mechanizing set theory: Cardinal arithmetic and the axiom of choice. Journal of Automated Reasoning, 17:291–323, 1996. find
  260. Lawrence C. Paulson. A higher-order implementation of rewriting. Science of Computer Programming, 3:119–149, 1983. find
  261. Lawrence C. Paulson. Logic and computation: interactive proof with Cambridge LCF, volume 2 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1987. find
  262. Lawrence C. Paulson. Isabelle: The next 700 theorem provers. In P. G. Odifreddi, editor, Logic and Computer Science, volume 31 of APIC Studies in Data Processing, pages 361–386. Academic Press, 1990. find
  263. Lawrence C. Paulson. A fixedpoint approach to implementing (co)inductive definitions. In Bundy [1994], pages 148–161. find
  264. Lawrence C. Paulson. Isabelle: a generic theorem prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994. With contributions by Tobias Nipkow. find
  265. Lawrence C. Paulson. The relative consistency of the axiom of choice mechanized using Isabelle/ZF. LMS Journal of Logic and Computation, 6:198–248, 2003. find
  266. Marko Petkovšek, Herbert S. Wilf, and Doron Zeilberger. A = B. A K Peters, 1996. find
  267. Frank Pfenning and Carsten Schürmann. System Description: Twelf – A Meta-Logical Framework for Deductive Systems. In Harald Ganzinger, editor, Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings, volume 1632 of LNCS, pages… find
  268. Frank Pfenning. Elf: A Meta-Language for Deductive Systems (System Des-crition). In Alan Bundy, editor, Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26 - July 1, 1994, Proceedings, volume 814 of LNCS, pages 811–815. Springer, 1994. find
  269. Wim Ploegaerts, Luc Claesen, and Hugo De Man. Defining recursive functions in HOL. In Archer et al. [1991], pages 358–366. find
  270. A. Pnueli. The temporal logic of programs. In Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pages 46–67, 1977. find
  271. Robert Pollack. The Theory of LEGO – A Proof Checker for the Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1994. find
  272. Vaughan Pratt. Every prime has a succinct certificate. SIAM Journal of Computing, 4:214–220, 1975. find
  273. Dag Prawitz, Håken Prawitz, and Neri Voghera. A mechanical proof procedure and its realization in an electronic computer. Journal of the ACM, 7:102–128, 1960. find
  274. J. P. Queille and J. Sifakis. Specification and verification of concurrent programs in CESAR. In Proceedings of the 5th International Symposium on Programming, volume 137 of Lecture Notes in Computer Science, pages 195–220. Springer-Verlag, 1982. John Harrison, Josef Urban and Freek Wiedijk find
  275. S. Rajan, N. Shankar, and M. K. Srivas. An integration of model-checking with automated proof-checking. In Pierre Wolper, editor, Computer-Aided Verification: CAV ’95, volume 939 of Lecture Notes in Computer Science, pages 84–97, Liege, Belgium, 1995. Springer-Verlag. find
  276. F. P. Ramsey. The foundations of mathematics. Proceedings of the London Mathematical Society (2), 25:338–384, 1926. find
  277. W. Reif. The KIV-approach to software verification. In M. Broy and S. Jähnichen, editors, KORSO: Methods, Languages and Tools for the Construction of Correct Software — Final Report, volume 1009 of Lecture Notes in Computer Science. Springer-Verlag, 1995. find
  278. J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12:23–41, 1965. find
  279. Rachel E. O. Roxas. A HOL package for reasoning about relations defined by mutual induction. In Joyce and Seger [1993], pages 129–140. find
  280. Piotr Rudnicki and Wlodzimierz Drabent. Proving properties of Pascal programs in MIZAR 2. Acta Inf., 22(3):311–331, 1985. find
  281. Piotr Rudnicki and Andrzej Trybulec. On equivalents of well-foundedness. J. Autom. Reasoning, 23(3-4):197–234, 1999. find
  282. Piotr Rudnicki and Andrzej Trybulec. On the integrity of a repository of formalized mathematics. In MKM, volume 2594 of Lecture Notes in Computer Science, pages 162–174. Springer, 2003. find
  283. Piotr Rudnicki. Obvious Inferences. Journal of Automated Reasoning, 3(4):383–393, 1987. find
  284. Piotr Rudnicki. Obvious inferences. Journal of Automated Reasoning, 3:383– 393, 1987. find
  285. John Rushby and Friedrich von Henke. Formal verification of algorithms for critical systems. In Proceedings of the Conference on Software for Critical Systems, pages 1–15. Association for Computing Machinery, 1991. find
  286. Bertrand Russell. Introduction to mathematical philosophy. Allen & Unwin, 1919. find
  287. David Russinoff. A mechanically checked proof of IEEE compliance of a register-transfer-level specification of the AMD-K7 floating-point multiplication, division, and square root instructions. LMS Journal of Computation and Mathematics, 1:148–200, 1998. Available on the Web at http://www.russinoff.c… ↗
  288. Jun Sawada and Ruben Gamboa. Mechanical verification of a square root algorithms using Taylor’s theorem. In M. Aagaard and John O’Leary, editors, Formal Methods in Computer-Aided Design: Fourth International Conference FMCAD 2002, volume 2517 of Lecture Notes in Computer Science, pages 274–291. Spri… find
  289. Mark Scheffer. The Automath Archive, 2003. find
  290. Klaus Schneider and Jens Brandt, editors. Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2007, volume 4732 of Lecture Notes in Computer Science, Kaiserslautern, Germany, 2007. Springer-Verlag. find
  291. Stephan Schulz. Learning search control knowledge for equational deduction, volume 230 of DISKI. Infix Akademische Verlagsgesellschaft, 2000. find
  292. Stephan Schulz. E - A Brainiac Theorem Prover. AI Commun., 15(2-3):111–126, 2002. find
  293. Dana Scott. A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical Computer Science, 121:411–440, 1993. Annotated version of a 1969 manuscript. find
  294. Carl-Johan H. Seger and Randal E. Bryant. Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design, 6:147–189, 1995. find
  295. Carl Seger and Jeffrey J. Joyce. A two-level formal verification methodology using HOL and COSMOS. Technical Report 91-10, Department of Computer Science, University of British Columbia, 2366 Main Mall, University of British Columbia, Vancouver, B.C, Canada V6T 1Z4, 1991. find
  296. Thomas Sewell, Magnus O. Myreen, and Gerwin Klein. Translation validation for a verified OS kernel. In Proceedings of the 34th ACM SIGPLAN conference on Programming language design and implementation, PLDI ’13, pages 471–482. Association for Computing Machinery, 2013. History of Interactive Theorem… find
  297. N. Shankar. Metamathematics, Machines and Gödel’s Proof, volume 38 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1994. find
  298. John Shawe-Taylor and Nello Cristianini. Kernel Methods for Pattern Analysis. Cambridge University Press, New York, NY, USA, 2004. find
  299. Robert Shostak. Deciding combinations of theories. Journal of the ACM, 31:1– 12, 1984. find
  300. J. Siekmann and G. Wrightson, editors. Automation of Reasoning — Classical Papers on Computational Logic, Vol. I (1957-1966). Springer-Verlag, 1983. find
  301. Konrad Slind. An implementation of higher order logic. Technical Report 91-419-03, University of Calgary Computer Science Department, 2500 University Drive N. W., Calgary, Alberta, Canada, TN2 1N4, 1991. Author’s Masters thesis. find
  302. Konrad Slind. Function definition in higher order logic. In Wright et al. [1996], pages 381–398. find
  303. Anna Slobodová. Challenges for formal verification in industrial setting. In Lubos Brim, Boudewijn R. Haverkort, Martin Leucker, and Jaco van de Pol, editors, Proceedings of 11th FMICS and 5th PDMC, volume 4346 of Lecture Notes in Computer Science, pages 1–22. Springer-Verlag, 2007. find
  304. Raymond M. Smullyan. Gödel’s Incompleteness Theorems, volume 19 of Oxford Logic Guides. Oxford University Press, 1992. find
  305. Stefan Soko lowski. A note on tactics in LCF. Technical Report CSR-140-83, University of Edinburgh, Department of Computer Science, 1983. find
  306. A. Solovyev and T. Hales. Verification of bounds of linear programs. In James H. Davenport, William M. Farmer, Florian Rabe, and Josef Urban, editors, Proceedings of CICM conference on intelligent computer mathematics, volume 6824 of Lecture Notes in Computer Science, pages 123–132. Springer-Verlag,… find
  307. Gunnar Stålmarck and M. Säflund. Modeling and verifying systems and software in propositional logic. In B. K. Daniels, editor, Safety of Computer Control Systems, 1990 (SAFECOMP ’90), pages 31–36, Gatwick, UK, 1990. Pergamon Press. find
  308. Mark Staples. Linking ACL2 and HOL. Technical Report 476, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK, 1999. find
  309. Mark E. Stickel. A Prolog Technology Theorem Prover: Implementation by an extended Prolog compiler. Journal of Automated Reasoning, 4:353–380, 1988. find
  310. Donald Syme. DECLARE: A prototype declarative proof system for higher order logic. Technical Report 416, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK, 1997. find
  311. Carst Tankink, Herman Geuvers, James McKinna, and Freek Wiedijk. Proviola: A tool for proof re-animation. In Autexier et al. [2010], pages 440–454. find
  312. Carst Tankink, Christoph Lange, and Josef Urban. Point-and-write. In Jeuring et al. [2012], pages 169–185. find
  313. Carst Tankink, Cezary Kaliszyk, Josef Urban, and Herman Geuvers. Formal mathematics on display: A wiki for Flyspeck. In Jacques Carette, David Aspinall, Christoph Lange, Petr Sojka, and Wolfgang Windsteiger, editors, MKM/Calculemus/DML, volume 7961 of Lecture Notes in Computer Science, pages 152–167… find
  314. Alfred Tarski. Der Wahrheitsbegriff in den formalisierten Sprachen. Studia Philosophica, 1:261–405, 1936. English translation, ‘The Concept of Truth in Formalized Languages’, in Tarski [1956], pp. 152–278. find
  315. Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285–309, 1955. find
  316. Alfred Tarski, editor. Logic, Semantics and Metamathematics. Clarendon Press, 1956. find
  317. Laurent Théry and Guillaume Hanrot. Primality proving with elliptic curves. In Schneider and Brandt [2007], pages 319–333. find
  318. Andrzej Trybulec. Informationslogische sprache Mizar. Dokumentation-Information: IX. Kolloquium über Information und Dokumentation vom 12. bis 14. November 1975, (33):46–53, 1977. find
  319. Andrzej Trybulec. The Mizar-QC/6000 logic information language. ALLC Bulletin, 6(2), 1978. John Harrison, Josef Urban and Freek Wiedijk find
  320. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. find
  321. Josef Urban and Geoff Sutcliffe. Automated reasoning and presentation support for formalizing mathematics in Mizar. In Autexier et al. [2010], pages 132–146. find
  322. Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jiřı́ Vyskočil. MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance. In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, IJCAR, volume 5195 of LNCS, pages 441–456. Springer, 2008. find
  323. Josef Urban, Jesse Alama, Piotr Rudnicki, and Herman Geuvers. A wiki for Mizar: Motivation, considerations, and initial prototype. In Autexier et al. [2010], pages 455–469. find
  324. Josef Urban, Jiřı́ Vyskočil, and Petr Štěpánek. MaLeCoP: Machine learning connection prover. In Kai Brünnler and George Metcalfe, editors, TABLEAUX, volume 6793 of LNCS, pages 263–277. Springer, 2011. find
  325. Josef Urban, Piotr Rudnicki, and Geoff Sutcliffe. ATP and presentation service for Mizar formalizations. J. Autom. Reasoning, 50:229–241, 2013. find
  326. Josef Urban. XML-izing Mizar: Making semantic processing and presentation of MML easy. In Michael Kohlhase, editor, MKM, volume 3863 of Lecture Notes in Computer Science, pages 346–360. Springer, 2005. find
  327. Josef Urban. MizarMode - an integrated proof assistance tool for the Mizar way of formalizing mathematics. Journal of Applied Logic, 4(4):414 – 427, 2006. find
  328. Josef Urban. MoMM - fast interreduction and retrieval in large libraries of formalized mathematics. Int. J. on Artificial Intelligence Tools, 15(1):109–130, 2006. find
  329. Christian Urban. Nominal techniques in Isabelle/HOL. JAR, 40:327–356, 2008. find
  330. Josef Urban. Parallelizing Mizar. CoRR, abs/1206.0141, 2012. — [arXiv:1206.0141](https://arxiv.org/abs/1206.0141) find
  331. Josef Urban. BliStr: The Blind Strategymaker. CoRR, abs/1301.2683, 2014. Accepted to PAAR’14. — [arXiv:1301.2683](https://arxiv.org/abs/1301.2683) find
  332. L.S. van Benthem Jutting. Checking Landau’s “Grundlagen” in the Automath system. Number 83 in Mathematical Centre Tracts. Mathematisch Centrum, Amsterdam, 1979. find
  333. Dirk van Dalen, editor. Brouwer’s Cambridge lectures on intuitionism. Cambridge University Press, 1981. find
  334. Mark van der Voort. Introducing well-founded function definitions in HOL. In Claesen and Gordon [1992], pages 117–132. find
  335. Konstantin Verchinine, Alexander Lyaletski, Andrei Paskevich, and Anatoly Anisimov. On correctness of mathematical texts from a logical and practical point of view. In Serge Autexier, John Campbell, Julio Rubio, Volker Sorge, Masakazu Suzuki, and Freek Wiedijk, editors, Intelligent Computer Mathemat… find
  336. Norbert Voelker. HOL2P — a system of classical higher order logic with second order polymorphism. In Schneider and Brandt [2007], pages 333–350. find
  337. Hao Wang. Toward mechanical mathematics. IBM Journal of Research and Development, 4:2–22, 1960. find
  338. Tjark Weber and Hasan Amjad. Efficiently checking propositional refutations in HOL theorem provers. Journal of Applied Logic, 7:26–40, 2009. find
  339. Tjark Weber. Validating QBF invalidity in HOL4. In Kaufmann and Paulson [2010], pages 466–480. find
  340. Roger Webster. Convexity. Oxford University Press, 1995. find
  341. Pierre Weis and Xavier Leroy. Le langage Caml. InterEditions, 1993. See also the CAML Web page: http://pauillac.inria.fr/caml/. ↗
  342. Markus Wenzel. Isar - a generic interpretive approach to readable formal proof documents. In Bertot et al. [1999], pages 167–183. find
  343. Makarius Wenzel. Isabelle/jEdit - a prover IDE within the PIDE framework. In Jeuring et al. [2012], pages 468–471. find
  344. Richard W. Weyhrauch and Carolyn Talcott. The logic of FOL systems: Formulated in set theory. In Neil D. Jones, Masami Hagiya, and Masahiko Sato, editors, Logic, Language and Computation: Festschrift in Honor of Satoru Takasu, volume 792 of Lecture Notes in Computer Science, pages 119–132. Springer… find
  345. Richard W. Weyhrauch. Prolegomena to a theory of mechanized formal reasoning. Artificial Intelligence, 13:133–170, 1980. find
  346. Richard W. Weyhrauch. An example of FOL using metatheory. In Donald W. Loveland, editor, Proceedings of the 6th Conference on Automated Deduction, number 138 in Lecture Notes in Computer Science, pages 151–158, New York, 1982. Springer Verlag. find
  347. Alfred North Whitehead and Bertrand Russell. Principia Mathematica (3 vols). Cambridge University Press, 1910. find
  348. Freek Wiedijk. CHECKER - notes on the basic inference step in Mizar. available at http://www.cs.kun.nl/∼freek/mizar/by.dvi, 2000. ↗
  349. Freek Wiedijk. Mizar light for HOL Light. In Richard J. Boulton and Paul B. Jackson, editors, 14th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2001, volume 2152 of Lecture Notes in Computer Science, pages 378–394. Springer-Verlag, 2001. find
  350. Freek Wiedijk. A New Implementation of Automath. J. Autom. Reasoning, 29(3-4):365–387, 2002. find
  351. Freek Wiedijk. The Seventeen Provers of the World, volume 3600 of Lecture Notes in Computer Science. Springer-Verlag, 2006. find
  352. Freek Wiedijk. Mizar’s soft type system. In Schneider and Brandt [2007], pages 383–399. find
  353. Freek Wiedijk. Statistics on digital libraries of mathematics. In Adam Grabowski and Adam Naumowicz, editors, Computer Reconstruction of the Body of Mathematics, volume 18(31) of Studies in Logic, Grammar and Rhetoric. University of Bia lystok, 2009. find
  354. Freek Wiedijk. Pollack inconsistency. Electronic Notes in Theoretical Computer Science, 285:85–100, 2012. find
  355. Freek Wiedijk. A synthesis of the procedural and declarative styles of interactive theorem proving. Logical Methods in Computer Science, 8(1), 2012. find
  356. Wai Wong. Recording HOL proofs. Technical Report 306, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK, 1993. find
  357. L. Wos, G. Robinson, D. Carson, and L. Shalla. The concept of demodulation in theorem proving. Journal of the ACM, 14:698–709, 1967. find
  358. Joakim von Wright, Jim Grundy, and John Harrison, editors. Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs’96, volume 1125 of Lecture Notes in Computer Science, Turku, Finland, 1996. Springer-Verlag. find
  359. Joakim von Wright. Representing higher-order logic proofs in HOL. In Thomas F. Melham and Juanito Camilleri, editors, Higher Order Logic Theorem Proving and Its Applications: Proceedings of the 7th International Workshop, volume 859 of Lecture Notes in Computer Science, pages 456–470, Valletta, Malt… find
  360. Wen-tsün Wu. On the decision problem and the mechanization of theorem proving in elementary geometry. Scientia Sinica, 21:157–179, 1978. find
  361. W. D. Young. System verification and the CLI stack. In Jonathan Bowen, editor, Towards Verified Systems. Elsevier Science Publications, 1993. find
  362. Gabriela Zalewska. Zamenhof, Ludwik (1859 – 1917). In The YIVO Encyclopedia of Jews in Eastern Europe. YIVO Institute for Jewish Research, 2010. find
  363. Vincent Zammit. On the implementation of an extensible declarative proof language. In Bertot et al. [1999], pages 185–202. INDEX Ωmega, 5 ⇒-elimination, 14 λ λ type theory, 9 K-match, 53 4-color theorem, 12, 57, 58 find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/harrison-2014-history-interactive-theorem-proving/