E.W.Ayers

PhD thesis
A Tool for Producing Verified, Explainable Proofs.

Abstract

Mathematicians are reluctant to use interactive theorem provers. In this thesis I argue that this is because proof assistants don't emphasise explanations of proofs; and that in order to produce good explanations, the system must create proofs in a manner that mimics how humans would create proofs. My research goals are to determine what constitutes a human-like proof and to represent human-like reasoning within an interactive theorem prover to create formalised, undersandable proofs. Another goal is to produce a framework to visualise the goal states of this system.

To demonstrate this, I present HumanProof: a piece of software built for the Lean 3 theorem prover. It is used for interactively creating proofs that resemble how human mathematicians reason. The system provides a visual, hierarchical representation of the goal and a system for suggesting available inference rules. The system produces output in the form of both natural language and formal proof terms which are checked by Lean's kernel. This is made possible with the use of a structured goal state system which interfaces with Lean's tactic system which is detailed in Chapter 3.

In Chapter 4, I present the subtasks automation planning subsystem, which is used to produce equality proofs in a human-like fashion. The basic strategy of the subtasks system is break a given equality problem in to a hierarchy of tasks and then maintain a stack of these tasks in order to determine the order in which to apply equational rewriting moves. This process produces equality chains for simple problems without having to resort to brute force or specialised procedures such as normalisation. This makes proofs more human-like by breaking the problem into a hierarchical set of tasks in the same way that a human would.

To produce the interface for this software, I also created the 'widgets' system for Lean 3. This system is detailed in Chapter 5. The widgets system utilises Lean's metaprogramming framework to allow users to write their own interactive, web-based user interfaces to display within the VSCode editor and in an online web-editor. This is also used to create interactive pretty-printing of expressions. The entire tactic state is available to the rendering engine, and hence expression structure and types of subexpressions can be explored interactively. The widgets system also allows the user interface to interactively edit the proof document, enabling a truly interactive modality for creating proofs; human-like or not.

In Chapter 6, the system is evaluated by asking real mathematicians about the output of the system, and what it means for a proof to be understandable to them. The user group study asks participants to rank and comment on proofs created by HumanProof alongside natural language and pure Lean proofs. The study finds that participants generally prefer the HumanProof format over the Lean format. The verbal responses collected during the study indicate that providing intuition and signposting are the most important properties of a proof that aid understanding.

Contents

Bibliography

There are 168 bibliography entries.

  • [ABB+16]Ahrendt, Wolfgang; Beckert, Bernhard; Bubel, Richard; Hähnle, Reiner; Schmitt, Peter H.; Ulbrich, MattiasDeductive Software Verification - The KeY Book (2016)publisher Springerdoi 10.1007/978-3-319-49812-6isbn 978-3-319-49811-9view online
  • [ADL10]Aspinall, David; Denney, Ewen; LĂĽth, ChristophTactics for hierarchical proof (2010)Mathematics in Computer Sciencevolume 3number 3pages 309--330publisher Springerview online
  • [AGJ19]Ayers, E. W.; Gowers, W. T.; Jamnik, MatejaA human-oriented term rewriting system (2019)KIpages 76--86organization Springerview online
  • [AH97]Archer, Myla; Heitmeyer, ConstanceHuman-style theorem proving using PVS (1997)International Conference on Theorem Proving in Higher Order Logicspages 33--48organization Springerview online
  • [AJG21]Ayers, E. W.; Jamnik, Mateja; Gowers, W. T.A graphical user interface framework for formal verification (2021)Interactive Theorem Proving
  • [ALW07]Aspinall, David; LĂĽth, Christoph; Winterstein, DanielA framework for interactive proof (2007)Towards Mechanized Mathematical Assistantspages 161--175publisher Springerview online
  • [AMM18]Adámek, Jiří; Milius, Stefan; Moss, Lawrence SFixed points of functors (2018)J. Log. Algebraic Methods Program.volume 95pages 41--81doi 10.1016/j.jlamp.2017.11.003view online
  • [AZHE10]Aigner, Martin; Ziegler, GĂĽnter M; Hofmann, Karl H; Erdos, PaulProofs from the Book (2010)publisher Springerisbn 978-3-662-57264-1view online
  • [Ano94]AnonymousThe QED manifesto (1994)Automated Deduction--CADEvolume 12pages 238--251view onlineUnofficially credited as Robert Boyer
  • [Asp00]Aspinall, DavidProof General: A generic tool for proof development (2000)International Conference on Tools and Algorithms for the Construction and Analysis of Systemspages 38--43organization Springerview online
  • [BBF+16]Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, AlbertSemi-intelligible Isar proofs from machine-generated proofs (2016)Journal of Automated Reasoningvolume 56number 2pages 155--200publisher Springerview online
  • [BBHI05]Bundy, Alan; Basin, David; Hutter, Dieter; Ireland, AndrewRippling: meta-level guidance for mathematical reasoning (2005)volume 56publisher Cambridge University Press
  • [BCC+13]Bainomugisha, Engineer; Carreton, Andoni Lombide; Cutsem, Tom van; Mostinckx, Stijn; Meuter, Wolfgang deA survey on reactive programming (2013)ACM Computing Surveys (CSUR)volume 45number 4pages 1--34publisher ACM New York, NY, USAview online
  • [BCF+97]BenzmĂĽller, Christoph; Cheikhrouhou, Lassaad; Fehrer, Detlef; Fiedler, Armin; Huang, Xiaorong; Kerber, Manfred; Kohlhase, Michael; Konrad, Karsten; Meier, Andreas; Melis, Erica; Schaarschmidt, Wolf; Siekmann, Jörg H.; Sorge, VolkerOmega: Towards a Mathematical Assistant (1997)Automated Deduction - CADE-14volume 1249pages 252--255editor McCune, Williampublisher Springerdoi 10.1007/3-540-63104-6_23view online
  • [BCJ+06]Buchberger, Bruno; CrÇŽciun, Adrian; Jebelean, Tudor; Kovács, Laura; Kutsia, Temur; Nakagawa, Koji; Piroi, Florina; Popov, Nikolaj; Robu, Judit; Rosenkranz, Markus; Windsteiger, WolfgangTheorema: Towards computer-aided mathematical theory exploration (2006)Journal of Applied Logicvolume 4number 4pages 470--504publisher Elsevierdoi 10.1016/j.jal.2005.10.006view online
  • [BE92]Barwise, Jon; Etchemendy, JohnHyperproof: Logical reasoning with diagrams (1992)Working Notes of the AAAI Spring Symposium on Reasoning with Diagrammatic Representationsview online
  • [BF97]Blum, Avrim L; Furst, Merrick LFast planning through planning graph analysis (1997)Artificial intelligencevolume 90number 1-2pages 281--300publisher Elsevierview online
  • [BG01]Bachmair, Leo; Ganzinger, HaraldResolution theorem proving (2001)Handbook of automated reasoningpages 19--99editors n.b.publisher Elsevier
  • [BGM+13]Bird, Richard; Gibbons, Jeremy; Mehner, Stefan; Voigtländer, Janis; Schrijvers, TomUnderstanding idiomatic traversals backwards and forwards (2013)Proceedings of the 2013 ACM SIGPLAN symposium on Haskellpages 25--36view online
  • [BJK+16]Buchberger, Bruno; Jebelean, Tudor; Kutsia, Temur; Maletzky, Alexander; Windsteiger, WolfgangTheorema 2.0: computer-assisted natural-style mathematics (2016)Journal of Formalized Reasoningvolume 9number 1pages 149--185view online
  • [BKM95]Boyer, Robert S; Kaufmann, Matt; Moore, J StrotherThe Boyer-Moore theorem prover and its interactive enhancement (1995)Computers & Mathematics with Applicationsvolume 29number 2pages 27--62publisher Elsevier
  • [BM72]Boyer, R. S.; Moore, J. S.The sharing structure in theorem-proving programs (1972)Machine intelligencevolume 7pages 101--116editors n.b.publisher Edinburgh University Pressview online
  • [BM73]Boyer, Robert S.; Moore, J. StrotherProving Theorems about LISP Functions (1973)IJCAIpages 486--493editor Nilsson, Nils J.publisher William Kaufmannview online
  • [BM90]Boyer, Robert S; Moore, J StrotherA theorem prover for a computational logic (1990)International Conference on Automated Deductionpages 1--15organization Springerview online
  • [BMR+20]Brown, Tom B.; Mann, Benjamin; Ryder, Nick; Subbiah, Melanie; Kaplan, Jared; Dhariwal, Prafulla; Neelakantan, Arvind; Shyam, Pranav; Sastry, Girish; Askell, Amanda; Agarwal, Sandhini; Herbert-Voss, Ariel; Krueger, Gretchen; Henighan, Tom; Child, Rewon; Ramesh, Aditya; Ziegler, Daniel M.; Wu, Jeffrey; Winter, Clemens; Hesse, Christopher; Chen, Mark; Sigler, Eric; Litwin, Mateusz; Gray, Scott; Chess, Benjamin; Clark, Jack; Berner, Christopher; McCandlish, Sam; Radford, Alec; Sutskever, Ilya; Amodei, DarioLanguage Models are Few-Shot Learners (2020)NeurIPSeditors n.b.view online
  • [BN10]Böhme, Sascha; Nipkow, TobiasSledgehammer: judgement day (2010)International Joint Conference on Automated Reasoningpages 107--121organization Springerview online
  • [BN98]Baader, Franz; Nipkow, TobiasTerm rewriting and all that (1998)publisher Cambridge University Pressisbn 978-0-521-45520-6
  • [BSV+93]Bundy, Alan; Stevens, Andrew; Van Harmelen, Frank; Ireland, Andrew; Smaill, AlanRippling: A heuristic for guiding inductive proofs (1993)Artificial Intelligencevolume 62number 2pages 185--253publisher Elsevier
  • [BT98]Bertot, Yves; ThĂ©ry, LaurentA generic approach to building user interfaces for theorem provers (1998)Journal of Symbolic Computationvolume 25number 2pages 161--194publisher Elsevierview online
  • [Bau20]Bauer, AndrejWhat makes dependent type theory more suitable than set theory for proof assistants? (2020)view onlineMathOverflow answer
  • [Bil05]Bille, PhilipA survey on tree edit distance and related problems (2005)Theoretical computer sciencevolume 337number 1-3pages 217--239publisher Elsevierview online
  • [Ble81]Bledsoe, Woodrow WNon-resolution theorem proving (1981)Readings in Artificial Intelligencepages 91--108publisher Elsevierview online
  • [Bre16]Breitner, JoachimVisual theorem proving with the Incredible Proof Machine (2016)International Conference on Interactive Theorem Provingpages 123--139publisher Springerview online
  • [Bun02]Bundy, AlanA critique of proof planning (2002)Computational Logic: Logic Programming and Beyondpages 160--177publisher Springerview online
  • [Bun11]Bundy, AlanAutomated theorem provers: a practical tool for the working mathematician? (2011)Annals of Mathematics and Artificial Intelligencevolume 61number 1pages 3doi 10.1007/s10472-011-9248-8view online
  • [Bun88]Bundy, AlanThe use of explicit plans to guide inductive proofs (1988)International conference on automated deductionpages 111--120organization Springerview online
  • [Bun98]Bundy, AlanProof planning (1998)publisher University of Edinburgh, Department of Artificial Intelligence
  • [CC13]Czaplicki, Evan; Chong, StephenAsynchronous functional reactive programming for GUIs (2013)ACM SIGPLAN Conference on Programming Language Design and Implementationpages 411--422editors n.b.publisher ACMdoi 10.1145/2491956.2462161view online
  • [CFK+09]Cramer, Marcos; Fisseni, Bernhard; Koepke, Peter; KĂĽhlwein, Daniel; Schröder, Bernhard; Veldman, JipThe naproche project controlled natural language proof checking of mathematical texts (2009)International Workshop on Controlled Natural Languagepages 170--186organization Springerview online
  • [CH88]Coquand, Thierry; Huet, GĂ©rard P.The Calculus of Constructions (1988)Inf. Comput.volume 76number 2/3pages 95--120doi 10.1016/0890-5401(88)90005-3view online
  • [CL18]Choi, Dongkyu; Langley, PatEvolution of the ICARUS cognitive architecture (2018)Cognitive Systems Researchvolume 48pages 25--38publisher Elsevier
  • [CMM+17]Corneli, Joseph; Martin, Ursula; Murray-Rust, Dave; Pease, Alison; Puzio, Raymond; Rino Nesin, GabrielaModelling the way mathematics is actually done (2017)Proceedings of the 5th ACM SIGPLAN International Workshop on Functional Art, Music, Modeling, and Designpages 10--19organization ACMview online
  • [Car19]Carneiro, MarioLean's Type Theory (2019)view online
  • [Chu18]Chua, DexterCambridge Notes (2018)view onlineGitHub: https://github.com/dalcde/cam-notes
  • [Com20]The Mathlib CommunityThe Lean Mathematical Library (2020)Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofspages 367–381publisher Association for Computing Machinerydoi 10.1145/3372885.3373824isbn 9781450370974view online
  • [Coq]The Coq Development TeamThe Coq Reference Manual (2021)view online
  • [DH93]Dalianis, Hercules; Hovy, EduardAggregation in natural language generation (1993)European Workshop on Trends in Natural Language Generationpages 88--105organization Springerview online
  • [DJP06]Dennis, Louise A; Jamnik, Mateja; Pollet, MartinOn the Comparison of Proof Planning Systems:, lambdaCLAM, Ωmega and IsaPlanner (2006)Proceedings of the 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoningvolume 151number 1pages 93--110editors n.b.publisher Elsevierdoi 10.1016/j.entcs.2005.11.025view online
  • [DKL20]De Lon, Adrian; Koepke, Peter; Lorenzen, AntonInterpreting Mathematical Texts in Naproche-SAD (2020)Intelligent Computer Mathematicspages 284--289editors n.b.publisher Springer International Publishingisbn 978-3-030-53518-6view online
  • [Dav09]Davis, Jared CurranA self-verifying theorem prover (2009)view online
  • [DeB80]De Bruijn, Nicolaas GovertA survey of the project AUTOMATH (1980)To H.B.Curry: Essays on Combinatory Logic,Lambda Calculus and Formalismpages 579-606editors n.b.publisher Academic Pressview online
  • [Dow01]Dowek, GilesHigher-order unification and matching (2001)Handbook of automated reasoningvolume 2pages 1009--1063editors n.b.publisher Elsevier
  • [EH97]Elliott, Conal; Hudak, PaulFunctional reactive animation (1997)Proceedings of the second ACM SIGPLAN international conference on Functional programmingpages 263--273view online
  • [EUR+17]Ebner, Gabriel; Ullrich, Sebastian; Roesch, Jared; Avigad, Jeremy; de Moura, LeonardoA metaprogramming framework for formal verification (2017)Proceedings of the ACM on Programming Languagesvolume 1number ICFPpages 1--29publisher ACM New York, NY, USAview online
  • [Edg07]Edgar, GeraldMeasure, topology, and fractal geometry (2007)publisher Springer Science and Business Media
  • [Ell01]Elliott, ConalFunctional Image Synthesis (2001)Proceedings of Bridgesview online
  • [FGM+07]Foster, J Nathan; Greenwald, Michael B; Moore, Jonathan T; Pierce, Benjamin C; Schmitt, AlanCombinators for bidirectional tree transformations: A linguistic approach to the view-update problem (2007)ACM Transactions on Programming Languages and Systems (TOPLAS)volume 29number 3pages 17--espublisher ACM New York, NY, USAview online
  • [FM87]Felty, Amy; Miller, DaleProof explanation and revision (1987)number MS-CIS-88-17institution University of Pennsylvaniaview online
  • [Fle19]Flet-Berliac, YannisThe Promise of Hierarchical Reinforcement Learning (2019)The Gradientview online
  • [GAA+13]Gonthier, Georges; Asperti, Andrea; Avigad, Jeremy; Bertot, Yves; Cohen, Cyril; Garillot, François; Le Roux, StĂ©phane; Mahboubi, Assia; O’Connor, Russell; Biha, Sidi Ould; othersA machine-checked proof of the odd order theorem (2013)International Conference on Interactive Theorem Provingpages 163--179organization Springerview online
  • [GFA09]Grossman, Tovi; Fitzmaurice, George; Attar, RamtinA survey of software learnability: metrics, methodologies and guidelines (2009)Proceedings of the SIGCHI Conference on Human Factors in Computing Systemspages 649--658view online
  • [GG17]Ganesalingam, Mohan; Gowers, W. T.A fully automatic theorem prover with human-style output (2017)J. Automated Reasoningvolume 58number 2pages 253--291doi 10.1007/s10817-016-9377-1view online
  • [GK18]Gatt, Albert; Krahmer, EmielSurvey of the state of the art in natural language generation: Core tasks, applications and evaluation (2018)Journal of Artificial Intelligence Researchvolume 61pages 65--170view online
  • [GKN15]Grabowski, Adam; KorniĹ‚owicz, Artur; Naumowicz, AdamFour decades of Mizar (2015)Journal of Automated Reasoningvolume 55number 3pages 191--198publisher Springerview online
  • [GM05]GrĂ©goire, Benjamin; Mahboubi, AssiaProving equalities in a commutative ring done right in Coq (2005)International Conference on Theorem Proving in Higher Order Logicspages 98--113organization Springerview online
  • [GPJ17]Gallego Arias, Emilio JesĂşs; Pin, BenoĂ®t; Jouvelot, PierrejsCoq: Towards Hybrid Theorem Proving Interfaces (2017)Proceedings of the 12th Workshop on User Interfaces for Theorem Proversvolume 239pages 15-27editors n.b.publisher Open Publishing Associationdoi 10.4204/EPTCS.239.2view online
  • [Gal16]Gallego Arias, Emilio JesĂşsSerAPI: Machine-Friendly, Data-Centric Serialization for Coq (2016)institution MINES ParisTechview online
  • [Gan10]Ganesalingam, MohanThe language of mathematics (2010)publisher Springerview online
  • [Gon05]Gonthier, GeorgesA computer-checked proof of the four colour theorem (2005)
  • [Gor00]Gordon, MikeFrom LCF to HOL: a short history (2000)Proof, language, and interactionpages 169--186view online
  • [Gow10]Gowers, W. T.Rough structure and classification (2010)Visions in Mathematicspages 79--117publisher Springerview online
  • [Gre19]Grebing, Sarah CaeciliaUser Interaction in Deductive Interactive Program Verification (2019)view online
  • [Gri75]Grice, Herbert PLogic and conversation (1975)Speech actspages 41--58publisher Brillview online
  • [HAB+17]Hales, Thomas C; Adams, Mark; Bauer, Gertrud; Dang, Dat Tat; Harrison, John; Hoang, Truong Le; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Thang Tat; Nguyen, Truong Quang; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason M.; Solovyev, Alexey; Ta, An Hoai Thi; Tran, Trung Nam; Trieu, Diep Thi; Urban, Josef; Vu, Ky Khac; Zumkeller, RolandA formal proof of the Kepler conjecture (2017)Forum of Mathematics, Pivolume 5organization Cambridge University Pressview online
  • [HBC99]Holland-Minkley, Amanda M; Barzilay, Regina; Constable, Robert LVerbalization of High-Level Formal Proofs. (1999)AAAI/IAAIpages 277--284editors n.b.publisher AAAI Press / The MIT Pressview online
  • [HF97]Huang, Xiaorong; Fiedler, ArminProof Verbalization as an Application of NLG (1997)IJCAI (2)pages 965--972view online
  • [HHPW96]Hall, Cordelia V; Hammond, Kevin; Peyton Jones, Simon L; Wadler, Philip LType classes in Haskell (1996)ACM Transactions on Programming Languages and Systems (TOPLAS)volume 18number 2pages 109--138publisher ACM New York, NY, USAview online
  • [HRW+21]Han, Jesse Michael; Rute, Jason; Wu, Yuhuai; Ayers, Edward W; Polu, StanislasProof Artifact Co-training for Theorem Proving with Language Models (2021)arXiv preprint arXiv:2102.06203view online
  • [Hal05]Hales, Thomas CA proof of the Kepler conjecture (2005)Annals of mathematicspages 1065--1185publisher Mathematics Department, Princeton Universityview online
  • [Hal07]Hales, Thomas CThe Jordan curve theorem, formally and informally (2007)The American Mathematical Monthlyvolume 114number 10pages 882--894publisher Taylor & Francisview online
  • [Har09]Harrison, JohnHOL Light: An Overview. (2009)TPHOLsvolume 5674pages 60--66organization Springer
  • [Hue97]Huet, GĂ©rardFunctional Pearl: The Zipper (1997)Journal of functional programmingvolume 7number 5pages 549--554publisher Cambridge University Pressview online
  • [Hur95]Hurkens, Antonius JCA simplification of Girard's paradox (1995)International Conference on Typed Lambda Calculi and Applicationspages 266--278organization Springer
  • [IA12]Inglis, Matthew; Alcock, LaraExpert and novice approaches to reading mathematical proofs (2012)Journal for Research in Mathematics Educationvolume 43number 4pages 358--390publisher National Council of Teachers of Mathematicsview online
  • [IJR99]Ireland, Andrew; Jackson, Michael; Reid, GordonInteractive proof critics (1999)Formal Aspects of Computingvolume 11number 3pages 302--325publisher Springerview online
  • [Ire92]Ireland, AndrewThe use of planning critics in mechanizing inductive proofs (1992)International Conference on Logic for Programming Artificial Intelligence and Reasoningpages 178--189organization Springerview online
  • [JR12]Jaskelioff, Mauro; Rypacek, OndrejAn Investigation of the Laws of Traversals (2012)Proceedings Fourth Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2012, Tallinn, Estoniavolume 76pages 40--49editors n.b.doi 10.4204/EPTCS.76.5view online
  • [Jam01]Jamnik, MatejaMathematical Reasoning with Diagrams: From Intuition to Automation (2001)publisher CSLI Press
  • [KB83]Knuth, Donald E; Bendix, Peter BSimple word problems in universal algebras (1983)Automation of Reasoningpages 342--376publisher Springerview online
  • [KEH+09]Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; Andronick, June; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, SimonseL4: Formal verification of an OS kernel (2009)Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principlespages 207--220organization ACM
  • [KKY95]Kambhampati, Subbarao; Knoblock, Craig A; Yang, QiangPlanning as refinement search: A unified framework for evaluating design tradeoffs in partial-order planning (1995)Artificial Intelligencevolume 76number 1pages 167--238view online
  • [KMM13]Kaufmann, Matt; Manolios, Panagiotis; Moore, J StrotherComputer-aided reasoning: ACL2 case studies (2013)volume 4publisher Springer Science & Business Media
  • [KSFS05]Kiselyov, Oleg; Shan, Chung-chieh; Friedman, Daniel P; Sabry, AmrBacktracking, interleaving, and terminating monad transformers: (functional pearl) (2005)ACM SIGPLAN Noticesvolume 40number 9pages 192--203publisher ACM New York, NY, USAview online
  • [Knu86]Knuth, Donald E.The TeXbook (1986)publisher Addison-Wesleyisbn 0-201-13447-0
  • [Kuh14]Kuhn, TobiasA survey and classification of controlled natural languages (2014)Computational linguisticsvolume 40number 1pages 121--170publisher MIT Pressview online
  • [LC20]Lample, Guillaume; Charton, FrançoisDeep Learning For Symbolic Mathematics (2020)ICLRpublisher OpenReview.netview online
  • [LCT08]Langley, Pat; Choi, Dongkyu; Trivedi, NishantIcarus user’s manual (2008)institution Institute for the Study of Learning and Expertiseview online
  • [LD97]Lowe, Helen; Duncan, DavidXBarnacle: Making theorem provers more accessible (1997)Automated Deduction—CADE-14pages 404--407publisher Springerview online
  • [LP03]Lämmel, Ralf; Peyton Jones, SimonScrap Your Boilerplate (2003)Programming Languages and Systems, First Asian Symposium, APLAS 2003, Beijing, China, November 27-29, 2003, Proceedingsvolume 2895pages 357editor Ohori, Atsushipublisher Springerdoi 10.1007/978-3-540-40018-9_23view online
  • [LR13]LĂĽth, Christoph; Ring, MartinA web interface for Isabelle: The next generation (2013)International Conference on Intelligent Computer Mathematicspages 326--329organization Springerview online
  • [LYWP21]Li, Wenda; Yu, Lei; Wu, Yuhuai; Paulson, Lawrence C.IsarStep: a Benchmark for High-level Mathematical Reasoning (2021)International Conference on Learning Representationsview online
  • [Lew17]Lewis, Robert Y.An Extensible Ad Hoc Interface between Lean and Mathematica (2017)Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, PxTP 2017, BrasĂ­lia, Brazil, 23-24 September 2017volume 262pages 23--37editors n.b.doi 10.4204/EPTCS.262.4view online
  • [Low97]Lowe, HelenEvaluation of a Semi-Automated Theorem Prover (Part I) (1997)view online
  • [MAKR15]de Moura, Leonardo; Avigad, Jeremy; Kong, Soonho; Roux, CodyElaboration in Dependent Type Theory (2015)CoRRvolume abs/1505.04324view online
  • [MB08]de Moura, Leonardo; Bjørner, NikolajZ3: An efficient SMT solver (2008)International conference on Tools and Algorithms for the Construction and Analysis of Systemspages 337--340organization Springer
  • [MDHW93]Monk, Andrew; Davenport, Lora; Haber, Jeanne; Wright, PeterImproving your human-computer interface: A practical technique (1993)publisher Prentice-Hall New York
  • [MKA+15]de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; Van Doorn, Floris; von Raumer, JakobThe Lean theorem prover (system description) (2015)International Conference on Automated Deductionpages 378--388organization Springerview online
  • [MP08]McBride, Conor; Paterson, RossApplicative programming with effects (2008)J. Funct. Program.volume 18number 1pages 1--13doi 10.1017/S0956796807006326view online
  • [MS99]Melis, Erica; Siekmann, JörgKnowledge-based proof planning (1999)Artificial Intelligencevolume 115number 1pages 65--105publisher Elsevierview online
  • [MUP80]de Millo, Richard A; Upton, Richard J; Perlis, Alan JSocial processes and proofs of theorems and programs (1980)The mathematical intelligencervolume 3number 1pages 31--40publisher Springerview online
  • [Mar84]Martin-Löf, PerIntuitionistic type theory (1984)volume 1publisher Bibliopolisisbn 978-88-7088-228-5view online
  • [McB00]McBride, ConorDependently typed functional programs and their proofs (2000)view online
  • [McC60]McCarthy, JohnRecursive functions of symbolic expressions and their computation by machine, Part I (1960)Communications of the ACMvolume 3number 4pages 184--195publisher ACM New York, NY, USAview online
  • [Mic78]Michener, Edwina RisslandUnderstanding understanding mathematics (1978)Cognitive sciencevolume 2number 4pages 361--383publisher Wiley Online Librarydoi https://doi.org/10.1207/s15516709cog0204_3view online
  • [Mil72]Milner, RobinLogic for computable functions description of a machine implementation (1972)institution Stanford Universityview online
  • [Nev74]Nevins, Arthur JA human oriented logic for automatic theorem-proving (1974)Journal of the ACM (JACM)volume 21number 4pages 606--621publisher ACM New York, NY, USAview online
  • [Nor08]Norell, UlfDependently typed programming in Agda (2008)International school on advanced functional programmingpages 230--266organization Springer
  • [PLB+17]Pease, Alison; Lawrence, John; Budzynska, Katarzyna; Corneli, Joseph; Reed, ChrisLakatos-style collaborative mathematics through dialectical, structured and abstract argumentation (2017)Artificial Intelligencevolume 246pages 181--219publisher Elsevierview online
  • [PP89]Pfenning, Frank; Paulin-Mohring, ChristineInductively defined types in the Calculus of Constructions (1989)International Conference on Mathematical Foundations of Programming Semanticspages 209--228organization Springerview online
  • [Pas07]Paskevich, AndreiThe syntax and semantics of the ForTheL language (2007)view online
  • [Pau89]Paulson, Lawrence CThe foundation of a generic theorem prover (1989)Journal of Automated Reasoningvolume 5number 3pages 363--397publisher Springerview online
  • [Pau98]Paulson, Lawrence CThe inductive approach to verifying cryptographic protocols (1998)Journal of computer securityvolume 6number 1-2pages 85--128publisher IOS Press
  • [Pau99]Paulson, Lawrence CA generic tableau prover and its integration with Isabelle (1999)Journal of Universal Computer Sciencevolume 5number 3pages 73--87view online
  • [Pit20]Pit-Claudel, ClĂ©mentUntangling mechanized proofs (2020)SLE 2020: Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineeringpages 155--174doi https://doi.org/10.1145/3426425.3426940view online
  • [Poi14]PoincarĂ©, HenriScience and method (1914)translator Halsted, George Brucepublisher Amazon (out of copyright)isbn 978-1534945906view onlineThe version at URL is translated by Francis Maitland
  • [Pro13]The Univalent Foundations ProgramHomotopy Type Theory: Univalent Foundations of Mathematics (2013)publisher Institute for Advanced Studyview online
  • [PĂłl62]PĂłlya, GeorgeMathematical Discovery (1962)publisher John Wiley & Sonsview online
  • [RD00]Reiter, Ehud; Dale, RobertBuilding natural language generation systems (2000)publisher Cambridge university pressview online
  • [RN10]Russell, Stuart J.; Norvig, PeterArtificial Intelligence - A Modern Approach (2010)publisher Pearson Educationisbn 978-0-13-207148-2view online
  • [RSS+20]Raggi, Daniel; Stapleton, Gem; Stockdill, Aaron; Jamnik, Mateja; Garcia, Grecia Garcia; Cheng, Peter C.-H.How to (Re)represent it? (2020)32nd IEEE International Conference on Tools with Artificial Intelligencepages 1224--1232publisher IEEEdoi 10.1109/ICTAI50040.2020.00185view online
  • [RV02]Riazanov, Alexandre; Voronkov, AndreiThe design and implementation of VAMPIRE (2002)AI communicationsvolume 15number 2, 3pages 91--110publisher IOS Press
  • [Ran94]Ranta, AarneSyntactic categories in the language of mathematics (1994)International Workshop on Types for Proofs and Programspages 162--182organization Springerview online
  • [Ran95]Ranta, AarneContext-relative syntactic categories and the formalization of mathematical text (1995)International Workshop on Types for Proofs and Programspages 231--248organization Springerview online
  • [Ros53]Rosser, J. BarkleyLogic for Mathematicians (1953)publisher McGraw-Hillisbn 978-0-486-46898-3
  • [SB01]Snyder, Wayne; Baader, FranzUnification theory (2001)Handbook of automated reasoningvolume 1pages 447--533editors n.b.publisher Elsevier
  • [SB18a]Steen, Alexander; BenzmĂĽller, ChristophThe higher-order prover Leo-III (2018)International Joint Conference on Automated Reasoningpages 108--116organization Springer
  • [SB18b]Sutton, Richard S; Barto, Andrew GReinforcement learning: An introduction (2018)publisher MIT pressview online
  • [SBRT18]Stathopoulos, Yiannos; Baker, Simon; Rei, Marek; Teufel, SimoneVariable Typing: Assigning Meaning to Variables in Mathematical Text (2018)NAACL-HLT 2018pages 303--312editors n.b.publisher Association for Computational Linguisticsdoi 10.18653/v1/n18-1028view online
  • [SCO95]Stenning, Keith; Cox, Richard; Oberlander, JonContrasting the cognitive effects of graphical and sentential logic teaching: reasoning, representation and individual differences (1995)Language and Cognitive Processesvolume 10number 3-4pages 333--354publisher Taylor & Francisview online
  • [SCV19]Schulz, Stephan; Cruanes, Simon; Vukmirović, PetarFaster, Higher, Stronger: E 2.3 (2019)Proc. of the 27th CADE, Natal, Brasilnumber 11716pages 495--507editor Fontaine, Pascalpublisher Springerview online
  • [SH17]Sterling, Jonathan; Harper, RobertAlgebraic Foundations of Proof Refinement (2017)arXiv preprint arXiv:1703.05215view online
  • [SHB+99]Siekmann, Jörg; Hess, Stephan; BenzmĂĽller, Christoph; Cheikhrouhou, Lassaad; Fiedler, Armin; Horacek, Helmut; Kohlhase, Michael; Konrad, Karsten; Meier, Andreas; Melis, Erica; Pollet, Martin; Sorge, VolkerLOUI: Lovely OMEGA user interface (1999)Formal Aspects of Computingvolume 11number 3pages 326--342publisher Springerview online
  • [SORS01]Shankar, Natarajan; Owre, Sam; Rushby, John M; Stringer-Calvert, Dave WJPVS prover guide (2001)Computer Science Laboratory, SRI International, Menlo Park, CAview online
  • [SP82]Smyth, Michael B; Plotkin, Gordon DThe category-theoretic solution of recursive domain equations (1982)SIAM Journal on Computingvolume 11number 4pages 761--783publisher SIAMview online
  • [ST16]Stathopoulos, Yiannos A; Teufel, SimoneMathematical information retrieval based on type embeddings and query expansion (2016)COLING 2016pages 2344--2355editors n.b.publisher ACLview online
  • [Sac74]Sacerdoti, Earl DPlanning in a hierarchy of abstraction spaces (1974)Artificial intelligencevolume 5number 2pages 115--135publisher Elsevierdoi 10.1016/0004-3702(74)90026-5view online
  • [Sch12]Schreier, MargritQualitative content analysis in practice (2012)publisher Sage publicationsview online
  • [Sie90]Sierpinska, AnnaSome remarks on understanding in mathematics (1990)For the learning of mathematicsvolume 10number 3pages 24--41publisher FLM Publishing Associationview online
  • [Sie94]Sierpinska, AnnaUnderstanding in mathematics (1994)volume 2publisher Psychology Press
  • [Spi11]Spiwack, ArnaudVerified computing in homological algebra, a journey exploring the power and limits of dependent type theory (2011)view online
  • [Spi87]Spinoza, BenedictThe chief works of Benedict de Spinoza (1887)translator Elwes, R.H.M.view online
  • [Ste17]Steele Jr., Guy L.It's Time for a New Old Language (2017)view onlineInvited talk at Clojure/Conj 2017. Slides: http://groups.csail.mit.edu/mac/users/gjs/6.945/readings/Steele-MIT-April-2017.pdf
  • [Tat77]Tate, AustinGenerating project networks (1977)IJCAIpages 888--893organization Morgan Kaufmann Publishers Inc.view online
  • [Tho92]Thomassen, CarstenThe Jordan-Schönflies theorem and the classification of surfaces (1992)The American Mathematical Monthlyvolume 99number 2pages 116--130publisher Taylor & Francisview online
  • [UM20]Ullrich, Sebastian; de Moura, LeonardoBeyond Notations: Hygienic Macro Expansion for Theorem Proving Languages (2020)Automated Reasoningpages 167--182editors n.b.publisher Springer International Publishingview online
  • [VKB18]Vicary, Jamie; Kissinger, Aleks; Bar, KrzysztofGlobular: an online proof assistant for higher-dimensional rewriting (2018)Logical Methods in Computer Sciencevolume 14publisher Episciences.orgview onlineproject website: http://ncatlab.org/nlab/show/Globular
  • [VLP07]Verchinine, Konstantin; Lyaletski, Alexander; Paskevich, AndreiSystem for Automated Deduction (SAD): a tool for proof verification (2007)International Conference on Automated Deductionpages 398--403organization Springerview online
  • [VLPA08]Verchinine, Konstantin; Lyaletski, Alexander; Paskevich, Andrei; Anisimov, AnatolyOn correctness of mathematical texts from a logical and practical point of view (2008)International Conference on Intelligent Computer Mathematicspages 583--598organization Springer
  • [VSP+17]Vaswani, Ashish; Shazeer, Noam; Parmar, Niki; Uszkoreit, Jakob; Jones, Llion; Gomez, Aidan N.; Kaiser, Lukasz; Polosukhin, IlliaAttention is All you Need (2017)Neural Information Processing Systemspages 5998--6008editors n.b.view online
  • [Wad03]Wadler, PhilipA prettier printer (2003)The Fun of Programming, Cornerstones of Computingpages 223--243editors n.b.publisher Palgrave MacMillanview online
  • [Wen12]Wenzel, MakariusIsabelle/jEdit-A Prover IDE within the PIDE Framework. (2012)AISC/MKM/Calculemuspages 468--471organization Springerview online
  • [Wen18]Wenzel, MakariusIsabelle/PIDE after 10 years of development (2018)UITP workshop: User Interfaces for Theorem Provers. view online
  • [Wen99]Wenzel, MakariusIsar-a generic interpretative approach to readable formal proof documents (1999)TPHOLsvolume 99pages 167--184organization Springer
  • [Wie00]Wiedijk, FreekThe de Bruijn Factor (2000)view online
  • [Wie07]Wiedijk, FreekThe QED manifesto revisited (2007)Studies in Logic, Grammar and Rhetoricvolume 10number 23pages 121--133view online
  • [Zha16]Zhan, BohuaAUTO2, a saturation-based heuristic prover for higher-order logic (2016)International Conference on Interactive Theorem Provingpages 441--456organization Springerview online
  • [deB72]de Bruijn, Nicolaas GovertLambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem (1972)Indagationes Mathematicae (Proceedings)volume 75number 5pages 381--392organization North-Hollandview online
© 2021 E.W.Ayers. Built with Gatsby