CoChat
Sign Up
Cited by 107Logic, programming, and type systemsLogic, Reasoning, and KnowledgeHistory of Computing Technologies

The DOI matches its Crossref record; 2 of the 2 references it cites were found in a registry or an index.

History of Interactive Theorem Proving

Harrison, John, Urban, Josef, Wiedijk, Freek·2014·Handbook of the History of Logic
DOI 10.1016/b978-0-444-51624-4.50004-6
Open this paper in CoChat — free account

Overview

Integrity signals

Registry

Crossref · 10.1016/b978-0-444-51624-4.50004-6

Cites

2 of 2 references verified0 citation errors · 0 not checkable

Statistics

Recomputing p-values needs the paper’s full text.

Verification

Claims the paper makes

We couldn’t retrieve this paper’s full text, so its claims and self-check weren’t run. The registry and citation checks still apply.

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • Previous methods to generate auxiliary constructions are based on hand-crafted templates and domain-specific heuristics and are limited to a subset of human experiences expressible in hard-coded rules.

    “Previous methods to generate them are based on hand-crafted templates and domain-specific heuristics8–12, and are, therefore, limited by a subset of human experiences expressible in hard-coded rules.”

    From Solving olympiad geometry without human demonstrations (2024) · cites this paper as [8]

Citations

Cites

Flagged first, then by citations

Research works printed but not linked: 113

  1. Agrawal, 2004, PRIMES is in P, Annals of Mathematics, 160, 781, 10.4007/annals.2004.160.781 · DOI
  2. Aitken, 1998, Interactive theorem proving: An empirical study of user activity, Journal of Symbolic Computation, 25, 263, 10.1006/jsco.1997.0175 · DOI
  3. Appel, 1976, Every planar map is four colorable, Bulletin of the American Mathematical Society, 82, 711, 10.1090/S0002-9904-1976-14122-5 · DOI
  4. Asperti, 2003, Mathematical Knowledge Management in HELM, Ann. Math. Artif. Intell., 38, 27, 10.1023/A:1022907629104 · DOI
  5. Avigad, 2007, A formally verified proof of the prime number theorem, ACM Transactions on Computational Logic, 9, 1
  6. Bancerek, 2002, A compendium of continuous lattices in Mizar, J. Autom. Reasoning, 29, 189, 10.1023/A:1021966832558 · DOI
  7. Barendregt, 1997, The impact of the lambda calculus on logic and computer science, Bulletin of Symbolic Logic, 3, 181, 10.2307/421013 · DOI
  8. Barringer, 1984, A logic covering undefinedness in program proofs, Acta Informatica, 21, 251, 10.1007/BF00264250 · DOI
  9. Bates, 1985, Proofs as programs, ACM Transactions on Programming Languages and Systems, 7, 113, 10.1145/2363.2528 · DOI
  10. Beckert, 1995, lean TAP : Lean, tableau-based deduction, Journal of Automated Reasoning, 15, 339, 10.1007/BF00881804 · DOI
  11. Bergstra, 2007, Meadows and the equational specification of division, Theoretical Computer Science, 410, 1261, 10.1016/j.tcs.2008.12.015 · DOI
  12. Bertot, 1998, A generic approach to building user interfaces for theorem provers, J. Symb. Comput., 25, 161, 10.1006/jsco.1997.0171 · DOI
  13. Bledsoe, 1974, A man-machine theorem-proving system, Artificial Intelligence, 5, 51, 10.1016/0004-3702(74)90009-5 · DOI
  14. Bridge, 2014, Machine learning for first-order theorem proving, Journal of Automated Reasoning, 1
  15. Bryant, 1986, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, C-35, 677, 10.1109/TC.1986.1676819 · DOI
  16. Buchberger, 1965, vol. 41, 475
  17. Bumcrot, 1965, On lattice complements, Proceedings of the Glasgow Mathematical Association, 7, 22, 10.1017/S2040618500035103 · DOI
  18. Bundy, 1991, Experiments with proof plans for induction, Journal of Automated Reasoning, 7, 303, 10.1007/BF00249016 · DOI
  19. Burch, 1992, Symbolic model checking: 1020 states and beyond, Information and Computation, 98, 142, 10.1016/0890-5401(92)90017-A · DOI
  20. Burstall, 1969, Proving properties of programs by structural induction, The Computer Journal, 12, 41, 10.1093/comjnl/12.1.41 · DOI
  21. Caprotti, 2001, Formal and efficient primality proofs by the use of computer algebra oracles, Journal of Symbolic Computation, 32, 55, 10.1006/jsco.2001.0457 · DOI
  22. Chaieb, 2008, Proof synthesis and reflection for linear arithmetic, Journal of Automated Reasoning, 41, 10.1007/s10817-008-9101-x · DOI
  23. Church, 1940, A formulation of the Simple Theory of Types, Journal of Symbolic Logic, 5, 56, 10.2307/2266170 · DOI
  24. Coquand, 1988, The calculus of constructions, Inf. Comput., 76, 95, 10.1016/0890-5401(88)90005-3 · DOI
  25. Curzon, 1995, Tracking design changes with formal machine-checked proof, The Computer Journal, 38, 91, 10.1093/comjnl/38.2.91 · DOI
  26. Davis, 1960, A computing procedure for quantification theory, Journal of the ACM, 7, 201, 10.1145/321033.321034 · DOI
  27. de Bruijn, 1968, The mathematical language AUTOMATH, its usage, and some of its extensions, Vol. 133, 29
  28. de Bruijn, 1979, Wees contextbewust in WOT, Euclides, 7
  29. Denzinger, 1996, Recording and Analysing Knowledge-Based Distributed Deduction Processes, Journal of Symbolic Computation, 21, 523, 10.1006/jsco.1996.0029 · DOI
  30. Dick, 2011, The work of proof in the age of human-machine collaboration, Isis, 102, 494, 10.1086/661623 · DOI
  31. Floyd, 1967, Assigning meanings to programs, 19, 10.1090/psapm/019/0235771 · DOI
  32. Geuvers, 1999, Some logical and syntactical observations concerning the first-order dependent type system lambda-P, Mathematical Structures in Computer Science, 9, 335, 10.1017/S0960129599002856 · DOI
  33. Gilmore, 1960, A proof method for quantification theory: Its justification and realization, IBM Journal of Research and Development, 4, 28, 10.1147/rd.41.0028 · DOI
  34. Gonthier, 2010, An introduction to small scale reflection in Coq, Journal of Formalized Reasoning, 3, 95
  35. Gonthier, 2008, Formal proof — the four-color theorem, Notices of the AMS, 35, 1382
  36. Good, 1979, An interactive program verification system, IEEE Transactions on Software Engineering, 1, 59
  37. Guard, 1969, Semi-automated mathematics, Journal of the ACM, 16, 49, 10.1145/321495.321500 · DOI
  38. Hales, 2010, A revision of the proof of the Kepler conjecture, Discrete and Computational Geometry, 44, 1, 10.1007/s00454-009-9148-4 · DOI
  39. Hales, 2005, A proof of the Kepler conjecture, Annals of Mathematics, 162, 1065, 10.4007/annals.2005.162.1065 · DOI
  40. Harrison, 1998, A sceptic’s approach to combining HOL and Maple, Journal of Automated Reasoning, 21, 279, 10.1023/A:1006023127567 · DOI
  41. Harrison, 2009, 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, 10.1007/s10817-009-9145-6 · DOI
  42. Heawood, 1890, Map-colour theorem, Quarterly Journal of Pure and Applied Mathematics, 24, 332
  43. Hoare, 1969, An axiomatic basis for computer programming, Communications of the ACM, 12, 576, 10.1145/363235.363259 · DOI
  44. Huet, 1975, A unification algorithm for typed λ-calculus, Theoretical Computer Science, 1, 27, 10.1016/0304-3975(75)90011-0 · DOI · Paper page
  45. Iverson, 1980, Notation as a tool of thought, Communications of the ACM, 23, 444, 10.1145/358896.358899 · DOI
  46. Jaśkowski, 1934, On the rules of supposition in formal logic, Studia Logica, 1, 5
  47. Kaliszyk, 2014, HOL(y)Hammer: Online ATP service for HOL Light, Mathematics in Computer Science, 10.1007/s11786-014-0182-0 · DOI
  48. Kaliszyk, 2014, Learning-assisted theorem proving with millions of lemmas, Journal of Symbolic Computation, 10.1016/j.jsc.2014.09.032 · DOI
  49. Kaliszyk, 2007, Web interfaces for proof assistants, Electr. Notes Theor. Comput. Sci, 174, 49, 10.1016/j.entcs.2006.09.021 · DOI
  50. Kaluzhnin, 1962, On an information language for mathematics, Applied Linguistic and Machine Translation, 21
  51. Kempe, 1879, On the geographical problem of the four colours, American Journal of Mathematics, 2, 193, 10.2307/2369235 · DOI
  52. Klein, 2010, seL4: Formal verification of an os kernel, Communications of the ACM, 53, 107, 10.1145/1743546.1743574 · DOI
  53. Knaster, 1927, Un théorème sur les fonctions d’ensembles, Annales de la Société Polonaise de Mathématique, 6, 133
  54. Krauss, 2010, Partial and nested recursive function definitions in higher-order logic, Journal of Automated Reasoning, 44, 303, 10.1007/s10817-009-9157-2 · DOI
  55. Kunen, 1998, Nonconstructive computational mathematics, Journal of Automated Reasoning, 21, 69, 10.1023/A:1005888712422 · DOI
  56. Lam, 1990, How reliable is a computer-based proof?, The Mathematical Intelligencer, 12, 8, 10.1007/BF03023977 · DOI
  57. Lamport, 1985, Synchronizing clocks in the presence of faults, Journal of the ACM, 32, 52, 10.1145/2455.2457 · DOI
  58. Landin, 1966, The next 700 programming languages, Communications of the ACM, 9, 157, 10.1145/365230.365257 · DOI
  59. Leroy, 2009, Formal verification of a realistic compiler, Communications of the ACM, 52, 107, 10.1145/1538788.1538814 · DOI
  60. Letichevsky, 2013, Glushkovs evidence algorithm, Cybernetics and Systems Analysis, 49, 489, 10.1007/s10559-013-9534-z · DOI
  61. London, 1970, Computer programs can be proved correct, 10.1007/978-3-642-99976-5_11 · DOI
  62. Loveland, 1968, Mechanical theorem-proving by model elimination, Journal of the ACM, 15, 236, 10.1145/321450.321456 · DOI
  63. Luo, 2003, PAL+: a lambda-free logical framework, J. Funct. Program., 13, 317, 10.1017/S0956796802004525 · DOI
  64. Marcus, 1985, SDVS: A system for verifying microcode correctness, ACM Sigsoft Software Engineering Notes, 10, 7, 10.1145/1012497.1012502 · DOI
  65. Ju, 1964, Maslov. An inverse method of establishing deducibility in classical predicate calculus, Doklady Akademii Nauk, 159, 17
  66. Matuszewski, 2005, Mizar: the first 30years, Mechanized Mathematics and Its Applications, 4, 3
  67. McCune, 1997, Solution of the Robbins problem, Journal of Automated Reasoning, 19, 263, 10.1023/A:1005843212881 · DOI
  68. Melliar-Smith, 1985, The Enhanced HDM system for specification and verification, ACM Software Engineering Notes, 10, 10.1145/1012497.1012511 · DOI
  69. Milner, 1972, Implementation and applications of Scott’s logic for computable functions, ACM SIGPLAN Notices, 7, 1, 10.1145/942578.807067 · DOI
  70. Milner, 1978, A theory of type polymorphism in programming, Journal of Computer and Systems Sciences, 17, 348, 10.1016/0022-0000(78)90014-4 · DOI
  71. Moore, 1998, A mechanically checked proof of the correctness of the kernel of the AM D5K86 floating-point division program, IEEE Transactions on Computers, 47, 913, 10.1109/12.713311 · DOI
  72. Naumowicz, 2002, Basic elements of computer algebra in MIZAR, Mechanized Mathematics and Its Applications, 2
  73. Naur, 1966, Proof of algorithms by general snapshots, BIT, 6, 310, 10.1007/BF01966091 · DOI
  74. Nelson, 1979, Simplification by cooperating decision procedures, ACM Transactions on Programming Languages and Systems, 1, 245, 10.1145/357073.357079 · DOI
  75. Nelson, 1980, Fast decision procedures based on congruence closure, Journal of the ACM, 27, 356, 10.1145/322186.322198 · DOI
  76. O’Leary, 1999, Formally verifying IEEE compliance of floating-point hardware, Intel Technology Journal, 1999-Q1, 1
  77. Parrilo, 2003, Semidefinite programming relaxations for semialgebraic problems, Mathematical Programming, 96, 293, 10.1007/s10107-003-0387-5 · DOI
  78. Patkowska, 1969, A homotopy extension theorem for fundamental sequences, Fundamenta Mathematicae, 64, 87, 10.4064/fm-64-1-87-89 · DOI
  79. Paulson, 1996, Mechanizing set theory: Cardinal arithmetic and the axiom of choice, Journal of Automated Reasoning, 17, 291, 10.1007/BF00283132 · DOI
  80. Paulson, 1983, A higher-order implementation of rewriting, Science of Computer Programming, 3, 119, 10.1016/0167-6423(83)90008-4 · DOI
  81. Paulson, 2003, The relative consistency of the axiom of choice mechanized using Isabelle/ZF, LMS Journal of Logic and Computation, 6, 198, 10.1112/S1461157000000449 · DOI
  82. Pratt, 1975, Every prime has a succinct certificate, SIAM Journal of Computing, 4, 214, 10.1137/0204018 · DOI
  83. Prawitz, 1960, A mechanical proof procedure and its realization in an electronic computer, Journal of the ACM, 7, 102, 10.1145/321021.321023 · DOI
  84. Ramsey, 1926, The foundations of mathematics, Proceedings of the London Mathematical Society (2), 25, 338, 10.1112/plms/s2-25.1.338 · DOI
  85. Robinson, 1965, A machine-oriented logic based on the resolution principle, Journal of the ACM, 12, 23, 10.1145/321250.321253 · DOI
  86. Rudnicki, 1985, Proving properties of Pascal programs in MIZAR 2, Acta Inf., 22, 311, 10.1007/BF00265684 · DOI
  87. Rudnicki, 1999, On equivalents of well-foundedness, J. Autom. Reasoning, 23, 197, 10.1023/A:1006218513245 · DOI
  88. Rudnicki, 1987, Obvious Inferences, Journal of Automated Reasoning, 3, 383, 10.1007/BF00247436 · DOI
  89. Rudnicki, 1987, Obvious inferences, Journal of Automated Reasoning, 3, 383, 10.1007/BF00247436 · DOI
  90. Russinoff, 1998, 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, 10.1112/S1461157000000176 · DOI
  91. Schulz, 2002, E - A Brainiac Theorem Prover, AI Commun, 15, 111
  92. Scott, 1993, A type-theoretical alternative to ISWIM, CUCH, OWHY, Theoretical Computer Science, 121, 411, 10.1016/0304-3975(93)90095-B · DOI
  93. Seger, 1995, Formal verification by symbolic evaluation of partially-ordered trajectories, Formal Methods in System Design, 6, 147, 10.1007/BF01383966 · DOI
  94. Shostak, 1984, Deciding combinations of theories, Journal of the ACM, 31, 1, 10.1145/2422.322411 · DOI
  95. Stickel, 1988, A Prolog Technology Theorem Prover: Implementation by an extended Prolog compiler, Journal of Automated Reasoning, 4, 353, 10.1007/BF00297245 · DOI
  96. Tarski, 1936, Der Wahrheitsbegriff in den formalisierten Sprachen, Studia Philosophica, 1, 261
  97. Tarski, 1955, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics, 5, 285, 10.2140/pjm.1955.5.285 · DOI
  98. Trybulec, 1977, Informationslogische sprache Mizar, Dokumentation-Information: IX. Kolloquium uber Information und Dokumentation vom 12. bis 14. November 1975, 46
  99. Trybulec, 1978, The Mizar-QC/6000 logic information language, ALLC Bulletin, 6
  100. Urban, 2013, ATP and presentation service for Mizar formalizations, J. Autom. Reasoning, 50, 229, 10.1007/s10817-012-9269-y · DOI
  101. Urban, 2006, MizarMode - an integrated proof assistance tool for the Mizar way of formalizing mathematics, Journal of Applied Logic, 4, 414, 10.1016/j.jal.2005.10.004 · DOI
  102. Urban, 2006, MoMM - fast interreduction and retrieval in large libraries of formalized mathematics, Int. J. on Artificial Intelligence Tools, 15, 109, 10.1142/S0218213006002588 · DOI
  103. Urban, 2008, Nominal techniques in Isabelle/HOL, JAR, 40, 327, 10.1007/s10817-008-9097-2 · DOI
  104. Urban, 2012, Parallelizing Mizar, CoRR
  105. Urban, 2014, BliStr: The Blind Strategymaker, CoRR
  106. Wang, 1960, Toward mechanical mathematics, IBM Journal of Research and Development, 4, 2, 10.1147/rd.41.0002 · DOI
  107. Weber, 2009, Efficiently checking propositional refutations in HOL theorem provers, Journal of Applied Logic, 7, 26, 10.1016/j.jal.2007.07.003 · DOI
  108. Weyhrauch, 1980, Prolegomena to a theory of mechanized formal reasoning, Artificial Intelligence, 13, 133, 10.1016/0004-3702(80)90015-6 · DOI
  109. Wiedijk, 2002, A New Implementation of Automath, J. Autom. Reasoning, 29, 365, 10.1023/A:1021983302516 · DOI
  110. Wiedijk, 2012, Pollack inconsistency, Electronic Notes in Theoretical Computer Science, 285, 85, 10.1016/j.entcs.2012.06.008 · DOI
  111. Wiedijk, 2012, A synthesis of the procedural and declarative styles of interactive theorem proving, Logical Methods in Computer Science, 8, 10.2168/LMCS-8(1:30)2012 · DOI
  112. Wos, 1967, The concept of demodulation in theorem proving, Journal of the ACM, 14, 698, 10.1145/321420.321429 · DOI
  113. Wu, 1978, On the decision problem and the mechanization of theorem proving in elementary geometry, Scientia Sinica, 21, 157

Cited by

Sorted by citations

Metadata

Authors
Harrison, J., Urban, J., & Wiedijk, F.
ORCID
Venue
Handbook of the History of Logic
Publisher
Elsevier
Published
2014
Pages
135-214
ISSN
1874-5857 (ISSN-L)
DOI
10.1016/b978-0-444-51624-4.50004-6
OpenAlex
W2549482841
Cited by
107
References
2
Citations by year
2026: 6 · 2025: 12 · 2024: 12 · 2023: 11 · 2022: 7 · 2021: 9 · 2020: 6 · 2019: 7 · 2018: 27 · 2017: 7 · 2016: 3
FWCI
17.93
Type
book chapter
Language
en
Open access
closed
Licence
www.elsevier.com/tdm/userlicense/1.0/ (tdm)
Locations
Handbook of the history of logic (publishedVersion)
Topics
  • Physical Sciences › Computer Science › Software › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, Reasoning, and Knowledge
  • Physical Sciences › Computer Science › Computer Science Applications › History of Computing Technologies
Keywords
interactive theorem proving, history of logic, automated reasoning, proof assistants, formal verification

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review