{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T13:05:23Z","timestamp":1777640723024,"version":"3.51.4"},"reference-count":382,"publisher":"Elsevier","isbn-type":[{"value":"9780444516244","type":"print"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1016\/b978-0-444-51624-4.50004-6","type":"book-chapter","created":{"date-parts":[[2014,12,9]],"date-time":"2014-12-09T19:00:55Z","timestamp":1418151655000},"page":"135-214","source":"Crossref","is-referenced-by-count":48,"title":["History of Interactive Theorem Proving"],"prefix":"10.1016","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Freek","family":"Wiedijk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0010","year":"2000"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0015","series-title":"Machine Verification of Mathematical Proof","author":"Abrahams","year":"1963"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0020","series-title":"The B-Book: Assigning Programs to Meanings","author":"Abrial","year":"1996"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0025","first-page":"142","article-title":"Introducing HOL Zero","author":"Adams","year":"2010"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0030","doi-asserted-by":"crossref","first-page":"781","DOI":"10.4007\/annals.2004.160.781","article-title":"PRIMES is in P","volume":"160","author":"Agrawal","year":"2004","journal-title":"Annals of Mathematics"},{"issue":"2","key":"10.1016\/B978-0-444-51624-4.50004-6_bb0035","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1006\/jsco.1997.0175","article-title":"Interactive theorem proving: An empirical study of user activity","volume":"25","author":"Aitken","year":"1998","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0040","series-title":"Calculemus\/MKM","first-page":"133","article-title":"Large formal wikis: Issues and solutions","author":"Alama","year":"2011"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0045","first-page":"95","article-title":"The semantics of reflected proof","author":"Allen","year":"1990"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0050","series-title":"Recursive boolean functions in HOL","first-page":"367","author":"Andersen","year":"1991"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0055","series-title":"Bundy","first-page":"238","article-title":"The QED Manifesto","author":"Anonymous","year":"1994"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0060","doi-asserted-by":"crossref","first-page":"711","DOI":"10.1090\/S0002-9904-1976-14122-5","article-title":"Every planar map is four colorable","volume":"82","author":"Appel","year":"1976","journal-title":"Bulletin of the American Mathematical Society"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0065","year":"1991"},{"issue":"1-3","key":"10.1016\/B978-0-444-51624-4.50004-6_bb0070","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1023\/A:1022907629104","article-title":"Mathematical Knowledge Management in HELM","volume":"38","author":"Asperti","year":"2003","journal-title":"Ann. Math. Artif. Intell."},{"key":"10.1016\/B978-0-444-51624-4.50004-6_rf0075","series-title":"TYPES","first-page":"17","article-title":"A content based mathematical search engine: Whelp","author":"Asperti","year":"2004"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0080","first-page":"18","article-title":"Crafting a proof assistant","author":"Asperti","year":"2006"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0085","series-title":"TACAS","first-page":"38","article-title":"Proof General: A generic tool for proof development","author":"Aspinall","year":"2000"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0090","year":"2010"},{"issue":"1:2","key":"10.1016\/B978-0-444-51624-4.50004-6_bb0095","first-page":"1","article-title":"A formally verified proof of the prime number theorem","volume":"9","author":"Avigad","year":"2007","journal-title":"ACM Transactions on Computational Logic"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0100","series-title":"Term Rewriting and All That","author":"Baader","year":"1998"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0105","series-title":"Correctness Preserving Program Transformations: Proof Theory and Applications","author":"Back","year":"1980"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0110","series-title":"Fix-point equations for well-founded recursion in type theory","first-page":"1","author":"Balaa","year":"2000"},{"issue":"3-4","key":"10.1016\/B978-0-444-51624-4.50004-6_bb0115","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1023\/A:1021966832558","article-title":"A compendium of continuous lattices in Mizar","volume":"29","author":"Bancerek","year":"2002","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0120","series-title":"MKM","first-page":"119","article-title":"Information retrieval in MML","author":"Bancerek","year":"2003"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0125","series-title":"MKM","first-page":"266","article-title":"Information retrieval and rendering with MML Query","author":"Bancerek","year":"2006"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0130","series-title":"Handbook of Logic in Computer Science (Vol. 2)","first-page":"117","article-title":"Lambda calculi with types","author":"Barendregt","year":"1992"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0135","doi-asserted-by":"crossref","first-page":"181","DOI":"10.2307\/421013","article-title":"The impact of the lambda calculus on logic and computer science","volume":"3","author":"Barendregt","year":"1997","journal-title":"Bulletin of Symbolic Logic"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0140","series-title":"Coq in Coq","author":"Barras","year":"1996"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0145","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/BF00264250","article-title":"A logic covering undefinedness in program proofs","volume":"21","author":"Barringer","year":"1984","journal-title":"Acta Informatica"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0150","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1145\/2363.2528","article-title":"Proofs as programs","volume":"7","author":"Bates","year":"1985","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0155","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1007\/BF00881804","article-title":"lean TAP : Lean, tableau-based deduction","volume":"15","author":"Beckert","year":"1995","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0160","series-title":"Foundations of constructive mathematics: metamathematical studies","author":"Beeson","year":"1984"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0165","series-title":"Inductive datatypes in HOL \u2013 lessons learned in formal-logic engineering","first-page":"19","author":"Berghofer","year":"1999"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0170","doi-asserted-by":"crossref","first-page":"1261","DOI":"10.1016\/j.tcs.2008.12.015","article-title":"Meadows and the equational specification of division","volume":"410","author":"Bergstra","year":"2007","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"10.1016\/B978-0-444-51624-4.50004-6_bb0175","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1006\/jsco.1997.0171","article-title":"A generic approach to building user interfaces for theorem provers","volume":"25","author":"Bertot","year":"1998","journal-title":"J. Symb. Comput."},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0180","series-title":"TACS","first-page":"141","article-title":"Proof by pointing","author":"Bertot","year":"1994"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_rf0185","year":"1999"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0190","series-title":"Graph Theory 1736-1936","author":"Biggs","year":"1976"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0195","series-title":"Current Trends in Hardware Verification and Automated Theorem Proving","year":"1989"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0200","series-title":"Constructive analysis","author":"Bishop","year":"1985"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0205","series-title":"TACAS","first-page":"493","article-title":"Encoding monomorphic and polymorphic types","author":"Blanchette","year":"2013"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0210","series-title":"Truly modular (co)datatypes for Isabelle\/HOL","first-page":"93","author":"Blanchette","year":"2014"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0215","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/0004-3702(74)90009-5","article-title":"A man-machine theorem-proving system","volume":"5","author":"Bledsoe","year":"1974","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0220","series-title":"Automatic theorem proof-checking in set theory: A preliminary report","author":"Bledsoe","year":"1967"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0225","series-title":"Automated Theorem Proving: After 25Years","first-page":"89","article-title":"Some automatic proofs in analysis","author":"Bledsoe","year":"1984"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0230","first-page":"1","article-title":"Program result checking: A new approach to making programs more reliable","author":"Blum","year":"1993"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0235","first-page":"107","article-title":"A formally-verified C compiler supporting floating-point arithmetic","author":"Boldo","year":"2013"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0240","first-page":"129","article-title":"Experience with embedding hardware description languages in HOL","author":"Boulton","year":"1993"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0245","series-title":"Boyer-Moore automation for the HOL system","first-page":"133","author":"Boulton","year":"1992"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0250","series-title":"Efficiency in a fully-expansive theorem prover","author":"Boulton","year":"1993"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0255","series-title":"Theory of sets","author":"Bourbaki","year":"1968"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0260","first-page":"73","article-title":"A Brief Overview of Agda - A Functional Language with Dependent Types","author":"Bove","year":"2009"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0265","series-title":"A Computational Logic","author":"Boyer","year":"1979"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0270","series-title":"The Correctness Problem in Computer Science","first-page":"103","article-title":"Metafunctions: proving them correct and using them efficiently as new proof procedures","author":"Boyer","year":"1981"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_rf0275","series-title":"A Computational Logic Handbook","author":"Boyer","year":"1988"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0280","first-page":"1","article-title":"Machine learning for first-order theorem proving","author":"Bridge","year":"2014","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0285","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-based algorithms for Boolean function manipulation","volume":"C-35","author":"Bryant","year":"1986","journal-title":"IEEE Transactions on Computers"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0290","first-page":"475","volume":"vol. 41","author":"Buchberger","year":"1965"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0295","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1017\/S2040618500035103","article-title":"On lattice complements","volume":"7","author":"Bumcrot","year":"1965","journal-title":"Proceedings of the Glasgow Mathematical Association"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0300","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/BF00249016","article-title":"Experiments with proof plans for induction","volume":"7","author":"Bundy","year":"1991","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0305","year":"1994"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0310","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","article-title":"Symbolic model checking: 1020 states and beyond","volume":"98","author":"Burch","year":"1992","journal-title":"Information and Computation"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0315","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1093\/comjnl\/12.1.41","article-title":"Proving properties of programs by structural induction","volume":"12","author":"Burstall","year":"1969","journal-title":"The Computer Journal"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0320","series-title":"Reasoning with inductively defined relations in the HOL theorem prover","author":"Camilleri","year":"1992"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0325","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1006\/jsco.2001.0457","article-title":"Formal and efficient primality proofs by the use of computer algebra oracles","volume":"32","author":"Caprotti","year":"2001","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0330","series-title":"The Logical Syntax of Language","author":"Carnap","year":"1937"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0335","series-title":"Twenty-five years of Constructive Type Theory","first-page":"57","article-title":"The Hahn-Banach Theorem in Type Theory","author":"Cederquist","year":"1998"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0340","doi-asserted-by":"crossref","DOI":"10.1007\/s10817-008-9101-x","article-title":"Proof synthesis and reflection for linear arithmetic","volume":"41","author":"Chaieb","year":"2008","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0345","series-title":"Tactic-based theorem proving and knowledge-based forward chaining","first-page":"552","author":"Chen","year":"1992"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0350","series-title":"Mechanical Geometry Theorem Proving","author":"Chou","year":"1988"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0355","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","article-title":"A formulation of the Simple Theory of Types","volume":"5","author":"Church","year":"1940","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0360","year":"1992"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0365","series-title":"Logics of Programs","first-page":"52","article-title":"Design and synthesis of synchronization skeletons using branching-time temporal logic","author":"Clarke","year":"1981"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0370","series-title":"Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Calculemus","first-page":"189","article-title":"A formal quantifier elimination for algebraically closed fields","author":"Cohen","year":"2010"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0375","series-title":"The Nearly Ultimate PEARL","author":"Constable","year":"1983"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0380","series-title":"A programming logic, with an introduction to the PL\/CV verifier","author":"Constable","year":"1978"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_rf0385","series-title":"Implementing Mathematics with The Nuprl Proof Development System","author":"Constable","year":"1986"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0390","series-title":"Machine Intelligence 7","first-page":"91","article-title":"Theorem proving in arithmetic without multiplication","author":"Cooper","year":"1972"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0395","series-title":"The Coq proof assistant reference manual","year":"2012"},{"issue":"2\/3","key":"10.1016\/B978-0-444-51624-4.50004-6_bb0400","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","article-title":"The calculus of constructions","volume":"76","author":"Coquand","year":"1988","journal-title":"Inf. Comput."},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0405","first-page":"50","article-title":"Inductively defined types","author":"Coquand","year":"1990"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0410","article-title":"An Emacs-Interface for Type-Directed Support for Constructing Proofs and Programs","author":"Coquand","year":"2005"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0415","series-title":"The Functional Approach to Programming","author":"Cousineau","year":"1998"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0420","series-title":"VDM \u201991: Formal Software Development Methods","first-page":"389","article-title":"EVES: An overview","author":"Craigen","year":"1991"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0425","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1093\/comjnl\/38.2.91","article-title":"Tracking design changes with formal machine-checked proof","volume":"38","author":"Curzon","year":"1995","journal-title":"The Computer Journal"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0430","series-title":"International Workshop on First-Order Theorem Proving","first-page":"58","article-title":"First order proof problems extracted from an article in the MIZAR mathematical library","author":"Dahn","year":"1997"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0435","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","article-title":"A computing procedure for quantification theory","volume":"7","author":"Davis","year":"1960","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0440","series-title":"Summaries of talks presented at the Summer Institute for Symbolic Logic, Cornell University","first-page":"215","article-title":"A computer program for Presburger\u2019s algorithm","author":"Davis","year":"1957"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0445","series-title":"IJCAI","first-page":"530","article-title":"Obvious logical inferences","author":"Davis","year":"1981"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0450","series-title":"A Self-Verifying Theorem Prover","author":"Davis","year":"2009"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0455","series-title":"AUTOMATH, a language for mathematics","author":"de Bruijn","year":"1968"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0460","series-title":"The mathematical language AUTOMATH, its usage, and some of its extensions","author":"de Bruijn","year":"1968"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0465","first-page":"29","article-title":"The mathematical language AUTOMATH, its usage, and some of its extensions","volume":"Vol. 133","author":"de Bruijn","year":"1968"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0470","series-title":"SEMIPAL 2, an extension of the mathematical notational language SEMIPAL","author":"de Bruijn","year":"1969"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0475","series-title":"A Processor for PAL","author":"de Bruijn","year":"1970"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0480","series-title":"Verslag over het project Wiskundige Taal AUTOMATH","author":"de Bruijn","year":"1978"},{"issue":"55","key":"10.1016\/B978-0-444-51624-4.50004-6_bb0485","first-page":"7","article-title":"Wees contextbewust in WOT","author":"de Bruijn","year":"1979","journal-title":"Euclides"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0490","series-title":"Gedachten rondom AUTOMATH","author":"de Bruijn","year":"1990"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_rf0495","first-page":"712","article-title":"Defining Lambda-Typed Lambda-Calculi by Axiomatizing the Typing Relation","author":"de Groote","year":"1993"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0500","series-title":"Automated Reasoning and Mathematics: Essays in Memory of William McCune","first-page":"15","article-title":"The strategy challenge in SMT solving","author":"de Moura","year":"2013"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0505","series-title":"Logic Programming and Automated Reasoning, LPAR 2000","first-page":"85","article-title":"A tactic language for the system Coq","author":"Delahaye","year":"2000"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0510","series-title":"A prototype proof translator from HOL to Coq","first-page":"108","author":"Denney","year":"2000"},{"issue":"4\/5","key":"10.1016\/B978-0-444-51624-4.50004-6_bb0515","doi-asserted-by":"crossref","first-page":"523","DOI":"10.1006\/jsco.1996.0029","article-title":"Recording and Analysing Knowledge-Based Distributed Deduction Processes","volume":"21","author":"Denzinger","year":"1996","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0520","doi-asserted-by":"crossref","first-page":"494","DOI":"10.1086\/661623","article-title":"The work of proof in the age of human-machine collaboration","volume":"102","author":"Dick","year":"2011","journal-title":"Isis"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0525","series-title":"Predicate Calculus and Program Semantics","author":"Dijkstra","year":"1990"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0530","series-title":"A Discipline of Programming","author":"Dijkstra","year":"1976"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0535","series-title":"A Proof Planning Framework for Isabelle","author":"Dixon","year":"2005"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0540","year":"2011"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0545","first-page":"502","article-title":"An extensible SAT-solver","author":"E\u00e9n","year":"2003"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0550","first-page":"681","article-title":"The Markgraf Karl refutation procedure (MKRP)","author":"Eisinger","year":"1986"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0555","first-page":"653","article-title":"IMPS: an interactive mathematical proof system","author":"Farmer","year":"1990"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0560","series-title":"Computers & Thought","year":"1995"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0565","series-title":"Automated Deduction \u2014 CADE-14","first-page":"351","article-title":"Hybrid interactive theorem proving using Nuprl and HOL","author":"Felty","year":"1997"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0570","series-title":"Symbolic Logic: an introduction","author":"Fitch","year":"1952"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0575","series-title":"A Combination of Geometry Theorem Proving and Nonstandard Analysis with Application to Newton\u2019s Principia","author":"Fleuriot","year":"2001"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0580","series-title":"Proceedings of AMS Symposia in Applied Mathematics, 19: Mathematical Aspects of Computer Science","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","article-title":"Assigning meanings to programs","author":"Floyd","year":"1967"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0585","year":"2006"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0590","series-title":"Temporal Logic","author":"Gabbay","year":"1994"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_rf0595","series-title":"Mechanically Verifying Real-Valued Algorithms in ACL2","author":"Gamboa","year":"1999"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0600","series-title":"The Language of Mathematics: A Linguistic and Philosophical Investigation","author":"Ganesalingam","year":"2013"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0605","first-page":"273","article-title":"Realization of a geometry-theorem proving machine","author":"Gelerntner","year":"1959"},{"issue":"4","key":"10.1016\/B978-0-444-51624-4.50004-6_bb0610","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1017\/S0960129599002856","article-title":"Some logical and syntactical observations concerning the first-order dependent type system lambda-P","volume":"9","author":"Geuvers","year":"1999","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0615","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1147\/rd.41.0028","article-title":"A proof method for quantification theory: Its justification and realization","volume":"4","author":"Gilmore","year":"1960","journal-title":"IBM Journal of Research and Development"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0620","series-title":"Meta-Programming in Logic Programming","first-page":"123","article-title":"Reflection in constructive and non-constructive automated reasoning","author":"Giunchiglia","year":"1989"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0625","series-title":"Design, Automation and Test in Europe Conference and Exhibition (DATE 2002)","first-page":"142","article-title":"BerkMin: a fast and robust Sat-solver","author":"Goldberg","year":"2002"},{"issue":"2","key":"10.1016\/B978-0-444-51624-4.50004-6_bb0630","first-page":"95","article-title":"An introduction to small scale reflection in Coq","volume":"3","author":"Gonthier","year":"2010","journal-title":"Journal of Formalized Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0635","series-title":"A Small Scale Reflection Extension for the Coq system","author":"Gonthier","year":"2008"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0640","first-page":"163","article-title":"A machine-checked proof of the odd order theorem","author":"Gonthier","year":"2013"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0645","first-page":"462","article-title":"Verifying the safety of a practical concurrent garbage collector","author":"Gonthier","year":"1996"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0650","series-title":"A computer-checked proof of the four colour theorem","author":"Gonthier","year":"2005"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0655","first-page":"1382","article-title":"Formal proof \u2014 the four-color theorem","volume":"35","author":"Gonthier","year":"2008","journal-title":"Notices of the AMS"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0660","first-page":"59","article-title":"An interactive program verification system","volume":"1","author":"Good","year":"1979","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0665","series-title":"Toward a Man-Machine System, for Proving Program Correctness","author":"Good","year":"1970"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0670","series-title":"Formal Specification: Proceedings of the Joint IBM\/University of Newcastle upon Tyne Seminar","first-page":"44","article-title":"Proof of a distributed system in Gypsy","author":"Good","year":"1983"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0675","series-title":"Recursive Number Theory","author":"Goodstein","year":"1957"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0680","series-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"Gordon","year":"1979"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0685","first-page":"153","article-title":"An integration of HOL and ACL2","author":"Gordon","year":"2006"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0690","series-title":"Tools and notions for program construction: an advanced course","first-page":"163","article-title":"Representing a logic in the LCF metalanguage","author":"Gordon","year":"1982"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_rf0695","series-title":"Why higher-order logic is a good formalism for specifying and verifying hardware","author":"Gordon","year":"1985"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0700","series-title":"Mechanizing programming logics in higher order logic","first-page":"387","author":"Gordon","year":"1989"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0705","series-title":"Proof, language, and interaction: essays in honour of Robin Milner","article-title":"From LCF to HOL: A short history","author":"Gordon","year":"2000"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0710","first-page":"97","article-title":"A computational approach to Pocklington certificates in type theory","author":"Gr\u00e9goire","year":"2006"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0715","first-page":"740","article-title":"Efs - an interactive environment for formal systems","author":"Griffin","year":"1988"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0720","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1145\/321495.321500","article-title":"Semi-automated mathematics","volume":"16","author":"Guard","year":"1969","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0725","series-title":"A broader class of trees for recursive type definitions for HOL","first-page":"141","author":"Gunter","year":"1993"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0730","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s00454-009-9148-4","article-title":"A revision of the proof of the Kepler conjecture","volume":"44","author":"Hales","year":"2010","journal-title":"Discrete and Computational Geometry"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0735","doi-asserted-by":"crossref","first-page":"1065","DOI":"10.4007\/annals.2005.162.1065","article-title":"A proof of the Kepler conjecture","volume":"162","author":"Hales","year":"2005","journal-title":"Annals of Mathematics"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0740","series-title":"Mathematics, Algorithms, Proofs","article-title":"Introduction to the Flyspeck project","author":"Hales","year":"2006"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0745","series-title":"Dense Sphere Packings: A Blueprint for Formal Proofs","author":"Hales","year":"2012"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0750","series-title":"Formal Aspects of VLSI Design: Proceedings of the 1985 Edinburgh Workshop on VLSI","first-page":"179","article-title":"Specification and verification using higher-order logic: A case study","author":"Hanna","year":"1986"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0755","first-page":"194","article-title":"A Framework for Defining Logics","author":"Harper","year":"1987"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0760","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1023\/A:1006023127567","article-title":"A sceptic\u2019s approach to combining HOL and Maple","volume":"21","author":"Harrison","year":"1998","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0765","first-page":"200","article-title":"Inductive definitions: automation and application","author":"Harrison","year":"1995"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0770","series-title":"Metatheory and reflection in theorem proving: A survey and critique","author":"Harrison","year":"1995"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0775","first-page":"265","article-title":"HOL Light: A tutorial introduction","author":"Harrison","year":"1996"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0780","series-title":"A Mizar mode for HOL","first-page":"203","author":"Harrison","year":"1996"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0785","series-title":"Types for Proofs and Programs: International Workshop TYPES\u201996","first-page":"154","article-title":"Proof style","author":"Harrison","year":"1996"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0790","series-title":"Theorem Proving with the Real Numbers","author":"Harrison","year":"1998"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_rf0795","first-page":"217","article-title":"Formal verification of floating point trigonometric functions","author":"Harrison","year":"2000"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0800","first-page":"159","article-title":"Complex quantifier elimination in HOL","author":"Harrison","year":"2001"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0805","first-page":"148","article-title":"Isolating critical cases for reciprocals using integer factorization","author":"Harrison","year":"2003"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0810","series-title":"The HOL Light tutorial","author":"Harrison","year":"2006"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0815","series-title":"Towards self-verification of HOL Light","first-page":"177","author":"Harrison","year":"2006"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0820","series-title":"Verifying nonlinear real formulas via sums of squares","first-page":"102","author":"Harrison","year":"2007"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0825","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/s10817-009-9145-6","article-title":"Formalizing an analytic proof of the Prime Number Theorem (dedicated to Mike Gordon on the occasion of his 60th birthday)","volume":"43","author":"Harrison","year":"2009","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0830","series-title":"Handbook of Practical Logic and Automated Reasoning","author":"Harrison","year":"2009"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0835","first-page":"332","article-title":"Map-colour theorem","volume":"24","author":"Heawood","year":"1890","journal-title":"Quarterly Journal of Pure and Applied Mathematics"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0840","series-title":"Elements of functional languages","author":"Henson","year":"1987"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0845","series-title":"ACM SIGCHI curricula for human-computer interaction","author":"Hewett","year":"1992"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0850","first-page":"287","article-title":"MetaPRL - A Modular Logical Environment","author":"Hickey","year":"2003"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0855","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","article-title":"An axiomatic basis for computer programming","volume":"12","author":"Hoare","year":"1969","journal-title":"Communications of the ACM"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0860","first-page":"130","article-title":"A design structure for higher order quotients","author":"Homeier","year":"2005"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0865","first-page":"244","article-title":"The HOL-Omega logic","author":"Homeier","year":"2009"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0870","series-title":"Proof Theory","first-page":"229","article-title":"Reflecting the semantics of reflected proof","author":"Howe","year":"1992"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0875","series-title":"Omega-MKRP: A proof development environment","first-page":"788","author":"Huang","year":"1994"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0880","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","article-title":"A unification algorithm for typed \u03bb-calculus","volume":"1","author":"Huet","year":"1975","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0885","first-page":"353","article-title":"Centaur Technology media unit verification","author":"Hunt","year":"2009"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_rf0890","series-title":"FM8501: A Verified Microprocessor","author":"Hunt","year":"1985"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0895","series-title":"Integrating Gandalf and HOL","first-page":"311","author":"Hurd","year":"1999"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0900","series-title":"Workshop on Design and Application of Strategies\/Tactics in Higher Order Logics","article-title":"First-order proof tactics in higher-order logic theorem provers","author":"Hurd","year":"2003"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0905","first-page":"177","article-title":"The OpenTheory standard theory library","author":"Hurd","year":"2010"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0910","doi-asserted-by":"crossref","first-page":"444","DOI":"10.1145\/358896.358899","article-title":"Notation as a tool of thought","volume":"23","author":"Iverson","year":"1980","journal-title":"Communications of the ACM"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0915","first-page":"5","article-title":"On the rules of supposition in formal logic","volume":"1","author":"Ja\u015bkowski","year":"1934","journal-title":"Studia Logica"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0920","series-title":"The Axiom of Choice","author":"Jech","year":"1973"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0925","series-title":"Pascal user manual and report","author":"Jensen","year":"1974"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0930","year":"2012"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0935","year":"1993"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0940","series-title":"Divider circuit verification with model checking and theorem proving","first-page":"338","author":"Kaivola","year":"2000"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0945","first-page":"196","article-title":"Proof engineering in the large: Formal verification of the Pentium (R) 4 floating-point divider","author":"Kaivola","year":"2001"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0950","first-page":"51","article-title":"Scalable LCF-style proof translation","author":"Kaliszyk","year":"2013"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0955","doi-asserted-by":"crossref","DOI":"10.1007\/s11786-014-0182-0","article-title":"HOL(y)Hammer: Online ATP service for HOL Light","author":"Kaliszyk","year":"2014","journal-title":"Mathematics in Computer Science"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0960","doi-asserted-by":"crossref","DOI":"10.1016\/j.jsc.2014.09.032","article-title":"Learning-assisted theorem proving with millions of lemmas","author":"Kaliszyk","year":"2014","journal-title":"Journal of Symbolic Computation"},{"issue":"2","key":"10.1016\/B978-0-444-51624-4.50004-6_bb0965","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/j.entcs.2006.09.021","article-title":"Web interfaces for proof assistants","volume":"174","author":"Kaliszyk","year":"2007","journal-title":"Electr. Notes Theor. Comput. Sci"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0970","first-page":"21","article-title":"On an information language for mathematics","author":"Kaluzhnin","year":"1962","journal-title":"Applied Linguistic and Machine Translation"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0975","year":"1992"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0980","year":"2010"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0985","series-title":"Computer-Aided Reasoning: ACL2 Case Studies","author":"Kaufmann","year":"2000"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb0990","series-title":"Computer-Aided Reasoning: An Approach","author":"Kaufmann","year":"2000"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_rf0995","series-title":"Importing HOL Light into Coq","first-page":"307","author":"Keller","year":"2010"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1000","doi-asserted-by":"crossref","first-page":"193","DOI":"10.2307\/2369235","article-title":"On the geographical problem of the four colours","volume":"2","author":"Kempe","year":"1879","journal-title":"American Journal of Mathematics"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1005","series-title":"A Program Verifier","author":"King","year":"1969"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1010","year":"2014"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1015","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1743546.1743574","article-title":"seL4: Formal verification of an os kernel","volume":"53","author":"Klein","year":"2010","journal-title":"Communications of the ACM"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1020","first-page":"133","article-title":"Un th\u00e9or\u00e8me sur les fonctions d\u2019ensembles","volume":"6","author":"Knaster","year":"1927","journal-title":"Annales de la Soci\u00e9t\u00e9 Polonaise de Math\u00e9matique"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1025","series-title":"Proceedings of the First Annual Symposium, on Logic in Computer Science","first-page":"237","article-title":"Formalized metareasoning in type theory","author":"Knoblock","year":"1986"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1030","series-title":"Computational Problems in Abstract Algebra","article-title":"Simple word problems in universal algebras","author":"Knuth","year":"1970"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1035","series-title":"AVID: a system for the interactive development of verifiably correct programs","author":"Krafft","year":"1981"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1040","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/s10817-009-9157-2","article-title":"Partial and nested recursive function definitions in higher-order logic","volume":"44","author":"Krauss","year":"2010","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1045","series-title":"IJCAR","first-page":"378","article-title":"Overview and evaluation of premise selection techniques for large theory mathematics","author":"K\u00fchlwein","year":"2012"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1050","series-title":"CADE","first-page":"407","article-title":"E-MaLeS 1.1","author":"K\u00fchlwein","year":"2013"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1055","series-title":"Validating QBF validity in HOL4","first-page":"168","author":"Kumar","year":"2011"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1060","series-title":"Integrating a first-order automatic prover in the HOL environment","first-page":"170","author":"Kumar","year":"1991"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1065","series-title":"HOL with definitions: Semantics, soundness and a verified implementation","first-page":"308","author":"Kumar","year":"2014"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1070","series-title":"Proving valid quantified boolean formulas in HOL Light","first-page":"184","author":"Kun\u010dar","year":"2011"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1075","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1023\/A:1005888712422","article-title":"Nonconstructive computational mathematics","volume":"21","author":"Kunen","year":"1998","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1080","series-title":"Proofs and Refutations: the Logic of Mathematical Discovery","author":"Lakatos","year":"1976"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1085","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1007\/BF03023977","article-title":"How reliable is a computer-based proof?","volume":"12","author":"Lam","year":"1990","journal-title":"The Mathematical Intelligencer"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1090","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1145\/2455.2457","article-title":"Synchronizing clocks in the presence of faults","volume":"32","author":"Lamport","year":"1985","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1095","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1145\/365230.365257","article-title":"The next 700 programming languages","volume":"9","author":"Landin","year":"1966","journal-title":"Communications of the ACM"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1100","series-title":"Erreurs de Math\u00e9maticiens des origines \u00e0 nos jours","author":"Lecat","year":"1935"},{"issue":"7","key":"10.1016\/B978-0-444-51624-4.50004-6_bb1105","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","article-title":"Formal verification of a realistic compiler","volume":"52","author":"Leroy","year":"2009","journal-title":"Communications of the ACM"},{"issue":"4","key":"10.1016\/B978-0-444-51624-4.50004-6_rf1110","doi-asserted-by":"crossref","first-page":"489","DOI":"10.1007\/s10559-013-9534-z","article-title":"Glushkovs evidence algorithm","volume":"49","author":"Letichevsky","year":"2013","journal-title":"Cybernetics and Systems Analysis"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1115","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-99976-5_11","article-title":"Computer programs can be proved correct","author":"London","year":"1970"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1120","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/321450.321456","article-title":"Mechanical theorem-proving by model elimination","volume":"15","author":"Loveland","year":"1968","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1125","series-title":"Automated theorem proving: a logical basis","author":"Loveland","year":"1978"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1130","first-page":"386","article-title":"ECC, an Extended Calculus of Constructions","author":"Luo","year":"1989"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1135","first-page":"293","article-title":"A unifying theory of dependent types: The schematic approach","author":"Luo","year":"1992"},{"issue":"2","key":"10.1016\/B978-0-444-51624-4.50004-6_bb1140","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1017\/S0956796802004525","article-title":"PAL+: a lambda-free logical framework","volume":"13","author":"Luo","year":"2003","journal-title":"J. Funct. Program."},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1145","series-title":"Evidence algorithm and system for automated deduction: A retrospective view","first-page":"411","author":"Lyaletski","year":"2010"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1150","series-title":"Mathematics: Form and Function","author":"Lane","year":"1986"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1155","series-title":"Mechanizing Proof: Computing, Risk and Trust","author":"MacKenzie","year":"2001"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1160","first-page":"213","article-title":"The ALF Proof Editor and Its Proof Engine","author":"Magnusson","year":"1993"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1165","series-title":"MKM 2007-Work in Progress","first-page":"47","article-title":"A document-oriented Coq plugin for TeXmacs","author":"Mamane","year":"2007"},{"issue":"4","key":"10.1016\/B978-0-444-51624-4.50004-6_bb1170","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1145\/1012497.1012502","article-title":"SDVS: A system for verifying microcode correctness","volume":"10","author":"Marcus","year":"1985","journal-title":"ACM Sigsoft Software Engineering Notes"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1175","series-title":"Intuitionistic type theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1180","first-page":"17","article-title":"Maslov. An inverse method of establishing deducibility in classical predicate calculus","volume":"159","author":"Ju","year":"1964","journal-title":"Doklady Akademii Nauk"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1185","first-page":"3","article-title":"Mizar: the first 30years","volume":"4","author":"Matuszewski","year":"2005","journal-title":"Mechanized Mathematics and Its Applications"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1190","series-title":"ONTIC: A Knowledge Representation System for Mathematics","author":"McAllester","year":"1989"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1195","first-page":"219","article-title":"Computer programs for checking mathematical proofs","author":"McCarthy","year":"1961"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1200","series-title":"Automated Deduction in Equational Logic and Cubic Curves","author":"McCune","year":"1996"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1205","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1023\/A:1005843212881","article-title":"Solution of the Robbins problem","volume":"19","author":"McCune","year":"1997","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1210","first-page":"295","article-title":"A proof-producing decision procedure for real arithmetic","author":"McLaughlin","year":"2005"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1215","article-title":"Cooperating theorem provers: A case study combining HOL-Light and CVC Lite","author":"Mclaughlin","year":"2005"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_rf1220","series-title":"An interpretation of Isabelle\/HOL in HOL Light","first-page":"192","author":"McLaughlin","year":"2006"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1225","first-page":"1","article-title":"Interpolation and SAT-based model checking","author":"McMillan","year":"2003"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1230","series-title":"Metamath: A computer language for pure mathematics","author":"Megill","year":"1996"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1235","series-title":"Automating recursive type definitions in higher order logic","first-page":"341","author":"Melham","year":"1989"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1240","series-title":"The HOL logic extended with quantification over type variables","first-page":"3","author":"Melham","year":"1992"},{"issue":"4","key":"10.1016\/B978-0-444-51624-4.50004-6_bb1245","doi-asserted-by":"crossref","DOI":"10.1145\/1012497.1012511","article-title":"The Enhanced HDM system for specification and verification","volume":"10","author":"Melliar-Smith","year":"1985","journal-title":"ACM Software Engineering Notes"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1250","series-title":"ESCoR: Empirically Succesful Computerized Reasoning","article-title":"Translating higher-order problems to first-order clauses","author":"Meng","year":"2006"},{"issue":"1","key":"10.1016\/B978-0-444-51624-4.50004-6_bb1255","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/942578.807067","article-title":"Implementation and applications of Scott\u2019s logic for computable functions","volume":"7","author":"Milner","year":"1972","journal-title":"ACM SIGPLAN Notices"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1260","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","article-title":"A theory of type polymorphism in programming","volume":"17","author":"Milner","year":"1978","journal-title":"Journal of Computer and Systems Sciences"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1265","series-title":"Automation of mathematical induction as part of the history of logic","author":"Moore","year":"2013"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1270","doi-asserted-by":"crossref","first-page":"913","DOI":"10.1109\/12.713311","article-title":"A mechanically checked proof of the correctness of the kernel of the AM D5K86 floating-point division program","volume":"47","author":"Moore","year":"1998","journal-title":"IEEE Transactions on Computers"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1275","series-title":"Programing from Specifications","author":"Morgan","year":"1990"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1280","series-title":"A theory of sets","author":"Morse","year":"1965"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1285","first-page":"530","article-title":"Chaff: Engineering an efficient SAT solver","author":"Moskewicz","year":"2001"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1290","series-title":"The reflective Milawa theorem prover is sound, down to the machine code that runs it","author":"Myreen","year":"2014"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1295","series-title":"TPHOLs","first-page":"329","article-title":"The HOL\/NuPRL proof translator (a practical approach to formal interoperability)","author":"Naumov","year":"2001"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1300","article-title":"Basic elements of computer algebra in MIZAR","volume":"2","author":"Naumowicz","year":"2002","journal-title":"Mechanized Mathematics and Its Applications"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1305","series-title":"MKM","first-page":"290","article-title":"Improving Mizar texts with properties and requirements","author":"Naumowicz","year":"2004"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1310","doi-asserted-by":"crossref","first-page":"310","DOI":"10.1007\/BF01966091","article-title":"Proof of algorithms by general snapshots","volume":"6","author":"Naur","year":"1966","journal-title":"BIT"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1315","series-title":"Automated Deduction \u2014 CADE-17","first-page":"25","article-title":"Proof generation in the Touchstone theorem prover","author":"Necula","year":"2000"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1320","series-title":"Selected papers on Automath","author":"Nederpelt","year":"1994"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1325","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","article-title":"Simplification by cooperating decision procedures","volume":"1","author":"Nelson","year":"1979","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1330","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","article-title":"Fast decision procedures based on congruence closure","volume":"27","author":"Nelson","year":"1980","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_rf1335","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1109\/TIT.1956.1056797","article-title":"The logic theory machine","volume":"2","author":"Newell","year":"1956","journal-title":"IRE Transactions on Information Theory"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1340","series-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"Nipkow","year":"2002"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1345","series-title":"Programming in Martin-L\u00f6f\u2019s Type Theory","author":"Nordstr\u00f6m","year":"1990"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1350","series-title":"Importing HOL into Isabelle\/HOL","first-page":"298","author":"Obua","year":"2006"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1355","first-page":"1","article-title":"Formally verifying IEEE compliance of floating-point hardware","volume":"1999-Q1","author":"O\u2019Leary","year":"1999","journal-title":"Intel Technology Journal"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1360","series-title":"FMCAD 2013: Formal Methods in Computer-Aided Design","first-page":"97","article-title":"Relational STE and theorem proving for formal verification of industrial circuit designs","author":"O\u2019Leary","year":"2013"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1365","series-title":"PVS: A prototype verification system","first-page":"748","author":"Owre","year":"1992"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1370","series-title":"On the automation of inductive proofs in HOL Light","author":"Papapanagiotou","year":"2007"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1375","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/s10107-003-0387-5","article-title":"Semidefinite programming relaxations for semialgebraic problems","volume":"96","author":"Parrilo","year":"2003","journal-title":"Mathematical Programming"},{"issue":"1","key":"10.1016\/B978-0-444-51624-4.50004-6_bb1380","doi-asserted-by":"crossref","first-page":"87","DOI":"10.4064\/fm-64-1-87-89","article-title":"A homotopy extension theorem for fundamental sequences","volume":"64","author":"Patkowska","year":"1969","journal-title":"Fundamenta Mathematicae"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1385","series-title":"Verified Software","first-page":"19","article-title":"Towards a worldwide verification techology","author":"Paul","year":"2008"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1390","first-page":"1","article-title":"Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers","author":"Paulson","year":"2010"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1395","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/BF00283132","article-title":"Mechanizing set theory: Cardinal arithmetic and the axiom of choice","volume":"17","author":"Paulson","year":"1996","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1400","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/0167-6423(83)90008-4","article-title":"A higher-order implementation of rewriting","volume":"3","author":"Paulson","year":"1983","journal-title":"Science of Computer Programming"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1405","series-title":"Logic and computation: interactive proof with Cambridge LCF","author":"Paulson","year":"1987"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1410","series-title":"Logic and Computer Science","first-page":"361","article-title":"Isabelle: The next 700 theorem provers","author":"Paulson","year":"1990"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1415","series-title":"A fixedpoint approach to implementing (co)inductive definitions","first-page":"148","author":"Paulson","year":"1994"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1420","series-title":"Isabelle: a generic theorem prover","author":"Paulson","year":"1994"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1425","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1112\/S1461157000000449","article-title":"The relative consistency of the axiom of choice mechanized using Isabelle\/ZF","volume":"6","author":"Paulson","year":"2003","journal-title":"LMS Journal of Logic and Computation"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1430","series-title":"A = B","author":"Petkov\u0161ek","year":"1996"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1435","first-page":"202","article-title":"System Description: Twelf - A Meta-Logical Framework for Deductive Systems","author":"Pfenning","year":"1999"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_rf1440","first-page":"811","article-title":"Elf: A Meta-Language for Deductive Systems (System Descrition)","author":"Pfenning","year":"1994"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1445","series-title":"Defining recursive functions in HOL","first-page":"358","author":"Ploegaerts","year":"1991"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1450","first-page":"46","article-title":"The temporal logic of programs","author":"Pnueli","year":"1977"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1455","series-title":"The Theory of LEGO - A Proof Checker for the Extended Calculus of Constructions","author":"Pollack","year":"1994"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1460","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1137\/0204018","article-title":"Every prime has a succinct certificate","volume":"4","author":"Pratt","year":"1975","journal-title":"SIAM Journal of Computing"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1465","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1145\/321021.321023","article-title":"A mechanical proof procedure and its realization in an electronic computer","volume":"7","author":"Prawitz","year":"1960","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1470","first-page":"195","article-title":"Specification and verification of concurrent programs in CESAR","author":"Queille","year":"1982"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1475","series-title":"Computer-Aided Verification: CAV \u201995","first-page":"84","article-title":"An integration of model-checking with automated proof-checking","author":"Rajan","year":"1995"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1480","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1112\/plms\/s2-25.1.338","article-title":"The foundations of mathematics","volume":"25","author":"Ramsey","year":"1926","journal-title":"Proceedings of the London Mathematical Society (2)"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1485","series-title":"KORSO: Methods, Languages and Tools for the Construction of Correct Software \u2014 Final Report","article-title":"The KIV-approach to software verification","author":"Reif","year":"1995"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1490","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine-oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1495","series-title":"A HOL package for reasoning about relations defined by mutual induction","first-page":"129","author":"Roxas","year":"1993"},{"issue":"3","key":"10.1016\/B978-0-444-51624-4.50004-6_bb1500","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1007\/BF00265684","article-title":"Proving properties of Pascal programs in MIZAR 2","volume":"22","author":"Rudnicki","year":"1985","journal-title":"Acta Inf."},{"issue":"3-4","key":"10.1016\/B978-0-444-51624-4.50004-6_bb1505","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1023\/A:1006218513245","article-title":"On equivalents of well-foundedness","volume":"23","author":"Rudnicki","year":"1999","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1510","series-title":"MKM","first-page":"162","article-title":"On the integrity of a repository of formalized mathematics","author":"Rudnicki","year":"2003"},{"issue":"4","key":"10.1016\/B978-0-444-51624-4.50004-6_bb1515","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1007\/BF00247436","article-title":"Obvious Inferences","volume":"3","author":"Rudnicki","year":"1987","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1520","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1007\/BF00247436","article-title":"Obvious inferences","volume":"3","author":"Rudnicki","year":"1987","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1525","series-title":"Proceedings of the Conference on Software for Critical Systems","first-page":"1","article-title":"Formal verification of algorithms for critical systems","author":"Rushby","year":"1991"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1530","series-title":"Introduction to mathematical philosophy","author":"Russell","year":"1919"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1535","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1112\/S1461157000000176","article-title":"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","volume":"1","author":"Russinoff","year":"1998","journal-title":"LMS Journal of Computation and Mathematics"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1540","first-page":"274","article-title":"Mechanical verification of a square root algorithms using Taylor\u2019s theorem","author":"Sawada","year":"2002"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1545","series-title":"The Automath Archive","author":"Scheffer","year":"2003"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_rf1550","year":"2007"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1555","series-title":"Learning search control knowledge for equational deduction","author":"Schulz","year":"2000"},{"issue":"2-3","key":"10.1016\/B978-0-444-51624-4.50004-6_bb1560","first-page":"111","article-title":"E - A Brainiac Theorem Prover","volume":"15","author":"Schulz","year":"2002","journal-title":"AI Commun"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1565","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1016\/0304-3975(93)90095-B","article-title":"A type-theoretical alternative to ISWIM, CUCH, OWHY","volume":"121","author":"Scott","year":"1993","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1570","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF01383966","article-title":"Formal verification by symbolic evaluation of partially-ordered trajectories","volume":"6","author":"Seger","year":"1995","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1575","series-title":"A two-level formal verification methodology using HOL and COSMOS","author":"Seger","year":"1991"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1580","first-page":"471","article-title":"Translation validation for a verified OS kernel","author":"Sewell","year":"2013"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1585","series-title":"Metamathematics, Machines and Godel\u2019s Proof","author":"Shankar","year":"1994"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1590","series-title":"Kernel Methods for Pattern Analysis","author":"Shawe-Taylor","year":"2004"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1595","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2422.322411","article-title":"Deciding combinations of theories","volume":"31","author":"Shostak","year":"1984","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1600","series-title":"Automation of Reasoning \u2014 Classical Papers on Computational Logic, Vol. I (1957-1966)","year":"1983"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1605","series-title":"An implementation of higher order logic","author":"Slind","year":"1991"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1610","series-title":"Function definition in higher order logic","first-page":"381","author":"Slind","year":"1996"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1615","series-title":"Proceedings of 11th FMICS and 5th PDMC","first-page":"1","article-title":"Challenges for formal verification in industrial setting","author":"Slobodov\u00e1","year":"2007"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1620","series-title":"G\u00f6del\u2019s Incompleteness Theorems","author":"Smullyan","year":"1992"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1625","series-title":"A note on tactics in LCF","author":"Soko\u0142owski","year":"1983"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1630","first-page":"123","article-title":"Verification of bounds of linear programs","author":"Solovyev","year":"2011"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1635","series-title":"Safety of Computer Control Systems, 1990 (SAFECOMP \u201990)","first-page":"31","article-title":"Modeling and verifying systems and software in propositional logic","author":"St\u00e5lmarck","year":"1990"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1640","series-title":"Linking ACL2 and HOL","author":"Staples","year":"1999"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1645","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","article-title":"A Prolog Technology Theorem Prover: Implementation by an extended Prolog compiler","volume":"4","author":"Stickel","year":"1988","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1650","series-title":"DECLARE: A prototype declarative proof system for higher order logic","author":"Syme","year":"1997"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_rf1655","series-title":"Proviola: A tool for proof re-animation","first-page":"440","author":"Tankink","year":"2010"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1660","series-title":"Point-and-write","first-page":"169","author":"Tankink","year":"2012"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1665","series-title":"MKM\/Calculemus\/DML","first-page":"152","article-title":"Formal mathematics on display: A wiki for Flyspeck","author":"Tankink","year":"2013"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1670","first-page":"261","article-title":"Der Wahrheitsbegriff in den formalisierten Sprachen","volume":"1","author":"Tarski","year":"1936","journal-title":"Studia Philosophica"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1675","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","article-title":"A lattice-theoretical fixpoint theorem and its applications","volume":"5","author":"Tarski","year":"1955","journal-title":"Pacific Journal of Mathematics"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1680","series-title":"Logic, Semantics and Metamathematics","year":"1956"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1685","series-title":"Primality proving with elliptic curves","first-page":"319","author":"Th\u00e9ry","year":"2007"},{"issue":"33","key":"10.1016\/B978-0-444-51624-4.50004-6_bb1690","first-page":"46","article-title":"Informationslogische sprache Mizar","author":"Trybulec","year":"1977","journal-title":"Dokumentation-Information: IX. Kolloquium uber Information und Dokumentation vom 12. bis 14. November 1975"},{"issue":"2","key":"10.1016\/B978-0-444-51624-4.50004-6_bb1695","article-title":"The Mizar-QC\/6000 logic information language","volume":"6","author":"Trybulec","year":"1978","journal-title":"ALLC Bulletin"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1700","series-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","year":"2013"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1705","series-title":"Automated reasoning and presentation support for formalizing mathematics in Mizar","first-page":"132","author":"Urban","year":"2010"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1710","series-title":"IJCAR","first-page":"441","article-title":"MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance","author":"Urban","year":"2008"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1715","series-title":"A wiki for Mizar: Motivation, considerations, and initial prototype","first-page":"455","author":"Urban","year":"2010"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1720","series-title":"TABLEAUX","first-page":"263","article-title":"MaLeCoP: Machine learning connection prover","author":"Urban","year":"2011"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1725","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1007\/s10817-012-9269-y","article-title":"ATP and presentation service for Mizar formalizations","volume":"50","author":"Urban","year":"2013","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1730","series-title":"MKM","first-page":"346","article-title":"XML-izing Mizar: Making semantic processing and presentation of MML easy","author":"Urban","year":"2005"},{"issue":"4","key":"10.1016\/B978-0-444-51624-4.50004-6_bb1735","doi-asserted-by":"crossref","first-page":"414","DOI":"10.1016\/j.jal.2005.10.004","article-title":"MizarMode - an integrated proof assistance tool for the Mizar way of formalizing mathematics","volume":"4","author":"Urban","year":"2006","journal-title":"Journal of Applied Logic"},{"issue":"1","key":"10.1016\/B978-0-444-51624-4.50004-6_bb1740","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1142\/S0218213006002588","article-title":"MoMM - fast interreduction and retrieval in large libraries of formalized mathematics","volume":"15","author":"Urban","year":"2006","journal-title":"Int. J. on Artificial Intelligence Tools"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1745","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1007\/s10817-008-9097-2","article-title":"Nominal techniques in Isabelle\/HOL","volume":"40","author":"Urban","year":"2008","journal-title":"JAR"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1750","article-title":"Parallelizing Mizar","author":"Urban","year":"2012","journal-title":"CoRR"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1755","article-title":"BliStr: The Blind Strategymaker","author":"Urban","year":"2014","journal-title":"CoRR"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1760","series-title":"Checking Landau\u2019s \u201cGrundlagen,\u201d in the Automath system","author":"van Benthem Jutting","year":"1979"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1765","series-title":"Brouwer\u2019s Cambridge lectures on intuitionism","year":"1981"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1770","series-title":"Introducing well-founded function definitions in HOL","first-page":"117","author":"van der Voort","year":"1992"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_rf1775","series-title":"Intelligent Computer Mathematics, AISC\/Calculemus\/MKM 2008","first-page":"583","article-title":"On correctness of mathematical texts from a logical and practical point of view","author":"Verchinine","year":"2008"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1780","series-title":"HOL2P \u2013 a system of classical higher order logic with second order polymorphism","first-page":"333","author":"Voelker","year":"2007"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1785","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1147\/rd.41.0002","article-title":"Toward mechanical mathematics","volume":"4","author":"Wang","year":"1960","journal-title":"IBM Journal of Research and Development"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1790","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1016\/j.jal.2007.07.003","article-title":"Efficiently checking propositional refutations in HOL theorem provers","volume":"7","author":"Weber","year":"2009","journal-title":"Journal of Applied Logic"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1795","series-title":"Validating QBF invalidity in HOL4","first-page":"466","author":"Weber","year":"2010"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1800","series-title":"Convexity","author":"Webster","year":"1995"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1805","series-title":"Le langage Caml","author":"Weis","year":"1993"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1810","series-title":"Isar - a generic interpretive approach to readable formal proof documents","first-page":"167","author":"Wenzel","year":"1999"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1815","series-title":"Isabelle\/jEdit - a prover IDE within the PIDE framework","first-page":"468","author":"Wenzel","year":"2012"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1820","series-title":"Logic, Language and Computation: Festschrift in Honor of Satoru Takasu","first-page":"119","article-title":"The logic of FOL systems: Formulated in set theory","author":"Weyhrauch","year":"1994"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1825","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/0004-3702(80)90015-6","article-title":"Prolegomena to a theory of mechanized formal reasoning","volume":"13","author":"Weyhrauch","year":"1980","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1830","first-page":"151","article-title":"An example of FOL using metatheory","author":"Weyhrauch","year":"1982"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1835","series-title":"Principia Mathematica (3 vols)","author":"Whitehead","year":"1910"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1840","series-title":"CHECKER - notes on the basic inference step in Mizar","author":"Wiedijk","year":"2000"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1845","first-page":"378","article-title":"Mizar light for HOL Light","author":"Wiedijk","year":"2001"},{"issue":"3-4","key":"10.1016\/B978-0-444-51624-4.50004-6_bb1850","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1023\/A:1021983302516","article-title":"A New Implementation of Automath","volume":"29","author":"Wiedijk","year":"2002","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1855","series-title":"The Seventeen Provers of the World","author":"Wiedijk","year":"2006"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1860","series-title":"Mizar\u2019s soft type system","first-page":"383","author":"Wiedijk","year":"2007"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1865","series-title":"Computer Reconstruction of the Body of Mathematics","article-title":"Statistics on digital libraries of mathematics","author":"Wiedijk","year":"2009"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1870","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/j.entcs.2012.06.008","article-title":"Pollack inconsistency","volume":"285","author":"Wiedijk","year":"2012","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"1","key":"10.1016\/B978-0-444-51624-4.50004-6_bb1875","doi-asserted-by":"crossref","DOI":"10.2168\/LMCS-8(1:30)2012","article-title":"A synthesis of the procedural and declarative styles of interactive theorem proving","volume":"8","author":"Wiedijk","year":"2012","journal-title":"Logical Methods in Computer Science"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1880","series-title":"Recording HOL proofs","author":"Wong","year":"1993"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1885","doi-asserted-by":"crossref","first-page":"698","DOI":"10.1145\/321420.321429","article-title":"The concept of demodulation in theorem proving","volume":"14","author":"Wos","year":"1967","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_rf1890","year":"1996"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1895","first-page":"456","article-title":"Representing higher-order logic proofs in HOL","author":"Wright","year":"1994"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1900","first-page":"157","article-title":"On the decision problem and the mechanization of theorem proving in elementary geometry","volume":"21","author":"Wu","year":"1978","journal-title":"Scientia Sinica"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1905","series-title":"Towards Verified Systems","article-title":"System verification and the CLI stack","author":"Young","year":"1993"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1910","series-title":"The YIVO Encyclopedia of Jews in Eastern Europe","article-title":"Zamenhof, Ludwik (1859 \u2013 1917)","author":"Zalewska","year":"2010"},{"key":"10.1016\/B978-0-444-51624-4.50004-6_bb1915","series-title":"On the implementation of an extensible declarative proof language","first-page":"185","author":"Zammit","year":"1999"}],"container-title":["Handbook of the History of Logic","Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444516244500046?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444516244500046?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,8,18]],"date-time":"2019-08-18T08:41:43Z","timestamp":1566117703000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780444516244500046"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9780444516244"],"references-count":382,"URL":"https:\/\/doi.org\/10.1016\/b978-0-444-51624-4.50004-6","relation":{},"ISSN":["1874-5857"],"issn-type":[{"value":"1874-5857","type":"print"}],"subject":[],"published":{"date-parts":[[2014]]}}}