{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:24:49Z","timestamp":1775053489650,"version":"3.50.1"},"reference-count":73,"publisher":"Elsevier","isbn-type":[{"value":"9780444508133","type":"print"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"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":[[2001]]},"DOI":"10.1016\/b978-044450813-3\/50015-1","type":"book-chapter","created":{"date-parts":[[2007,6,11]],"date-time":"2007-06-11T13:04:11Z","timestamp":1181567051000},"page":"845-911","source":"Crossref","is-referenced-by-count":71,"title":["The Automation of Proof by Mathematical Induction"],"prefix":"10.1016","author":[{"given":"Alan","family":"Bundy","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/B978-044450813-3\/50015-1_bb0010","article-title":"Mechanizing Structural Induction","author":"Aubin","year":"1976","journal-title":"PhD thesis, University of Edinburgh"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0015","series-title":"Proc. 13th Intern. Joint Conference on Artificial Intelligence (IJCAI '93)","first-page":"116","article-title":"Difference unification","author":"Basin","year":"1993"},{"issue":"1-2","key":"10.1016\/B978-044450813-3\/50015-1_bb0020","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF00244462","article-title":"A calculus for and termination of rippling","volume":"16","author":"Basin","year":"1996","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0025","series-title":"14th International Conference on Automated Deduction","first-page":"252","article-title":"\u0398mega: Towards a mathematical assistant","author":"Benzm\u00fcller","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0030","series-title":"Eighth European Conference on Artificial Intelligence","first-page":"553","article-title":"Automated synthesis of recursive algorithms as a theorem proving tool","author":"Biundo","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0035","series-title":"8th International Conference on Automated Deduction","first-page":"672","article-title":"The Karlsruhe induction theorem proving system","author":"Biundo","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0040","series-title":"\u2018Proceedings of the third IJCAI', International Joint Conference on Artificial Intelligence","first-page":"486","article-title":"Proving theorems about LISP functions","author":"Boyer","year":"1973"},{"key":"10.1016\/B978-044450813-3\/50015-1_rf0040","article-title":"A Computational Logic","author":"Boyer","year":"1979"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0050","series-title":"Perspectives in Computing","article-title":"A Computational Logic Handbook","author":"Boyer","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0055","series-title":"Machine Intelligence 11","first-page":"83","article-title":"Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic","author":"Boyer","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0060","series-title":"Formal Methods in Computer-Aided Design (FMCAD'96)","first-page":"275","article-title":"Acl2 theorems about commercial micro-processors","author":"Brock","year":"1996"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50015-1_bb0065","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","article-title":"Symbolic boolean manipulation with ordered binary-decision diagrams","volume":"24","author":"Bryant","year":"1992","journal-title":"ACM Computing Surveys"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0070","series-title":"9th International Conference on Automated Deduction","first-page":"111","article-title":"The use of explicit plans to guide inductive proofs","author":"Bundy","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0075","series-title":"Computational Logic: Essays in Honor of Alan Robinson","first-page":"178","article-title":"A science of reasoning","author":"Bundy","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0080","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","article-title":"Rippling: A heuristic for guiding inductive proofs","volume":"62","author":"Bundy","year":"1993","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0085","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-044450813-3\/50015-1_bb0090","series-title":"Proceedings of the Eleventh International Joint Conference on Artificial Intelligence","first-page":"359","article-title":"A rational reconstruction and extension of recursion analysis","author":"Bundy","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0095","series-title":"10th International Conference on Automated Deduction","first-page":"647","article-title":"The Oyster-Clam system","author":"Bundy","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0100","series-title":"10th International Conference on Automated Deduction","first-page":"132","article-title":"Extensions to the rippling-out tactic for guiding inductive proofs","author":"Bundy","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0105","first-page":"1635","article-title":"Model checking","volume":"Vol. II","author":"Clarke","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0110","series-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0115","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00264597","article-title":"A synthesis of several sorting algorithms","volume":"11","author":"Darlington","year":"1978","journal-title":"Acta Informatica"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0120","series-title":"Proceedings of AISB-80","article-title":"The MarkGraf Karl Refutation Procedure","author":"Eisinger","year":"1980"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0125","first-page":"1791","article-title":"Resolution decision procedures,","volume":"Vol. II","author":"Ferm\u00fcller","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0130","series-title":"\u2018Proceedings of ECAI-92', European Conference on Artificial Intelligence","first-page":"87","article-title":"Predicate synthesis from formal specifications","author":"Franova","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0135","article-title":"The Collected Papers of Gerhard Gentzen","author":"Gentzen","year":"1969"},{"key":"10.1016\/B978-044450813-3\/50015-1_rf0135","article-title":"\u00dcber formal unentscheidbare s\u00e4tze der principia mathematica und verwandter systeme i","volume":"38","author":"G\u00f6del","year":"1931","journal-title":"Monatsh. Math. Phys."},{"key":"10.1016\/B978-044450813-3\/50015-1_rf0140","first-page":"173","article-title":"From Frege to G\u00f6del: a source book in Mathematical Logic, 1879\u20131931","author":"Heijenoort","year":"1967"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0145","series-title":"Edinburgh LCF - A mechanised logic of computation","author":"Gordon","year":"1979"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0150","series-title":"From Frege to G\u00f6del: a source book in Mathematical Logic, 1879\u20131931","author":"Heijenoort","year":"1967"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0155","article-title":"Using Middle-Out Reasoning to Guide Inductive Theorem Proving","author":"Hesketh","year":"1991","journal-title":"PhD thesis, University of Edinburgh"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0160","series-title":"To H. B. Curry; Essays on Combinatory Logic, Lambda Calculus and Formalism","first-page":"479","article-title":"The formulae-as-types notion of construction","author":"Howard","year":"1980"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0165","article-title":"Generation of induction axioms and generalisation","author":"Hummel","year":"1990","journal-title":"PhD thesis, Universit\u00e4t Karlsruhe"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0170","series-title":"10th International Conference on Automated Deduction","first-page":"147","article-title":"Guiding inductive proofs","author":"Hutter","year":"1990"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50015-1_bb0175","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1023\/A:1005772217686","article-title":"Coloring terms to control equational reasoning","volume":"18","author":"Hutter","year":"1997","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0180","series-title":"14th International Conference on Automated Deduction","first-page":"291","article-title":"A colored version of the \u03bb-Calculus","author":"Hutter","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0185","series-title":"Formal Methods Europe '96","article-title":"Deduction in the verification support environment","author":"Hutter","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0190","series-title":"13th International Conference on Automated Deduction","first-page":"288","article-title":"INKA: the next generation","author":"Hutter","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0195","series-title":"International Conference on Logic Programming and Automated Reasoning \u2013 LPAR 92","first-page":"178","article-title":"The Use of Planning Critics in Mechanizing Inductive Proofs","author":"Ireland","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0200","series-title":"13th International Conference on Automated Deduction","first-page":"47","article-title":"Extensions to a Generalization Critic for Inductive Proof","author":"Ireland","year":"1996"},{"issue":"1-2","key":"10.1016\/B978-044450813-3\/50015-1_bb0205","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BF00244460","article-title":"Productive use of failure in inductive proof","volume":"16","author":"Ireland","year":"1996","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0210","series-title":"8th International Conference on Automated Deduction","first-page":"692","article-title":"RRL: A rewrite rule laboratory","author":"Kapur","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0215","series-title":"13th International Conference on Automated Deduction (CADE-13)","first-page":"538","article-title":"Lemma discovery in automating induction","author":"Kapur","year":"1996"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50015-1_bb0220","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1016\/0898-1221(94)00218-A","article-title":"An overview of rewrite rule laboratory (RRL)","volume":"29","author":"Kapur","year":"1995","journal-title":"J. of Computer Mathematics with Applications"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0225","article-title":"A user's manual for an interactive enhancement to the Boyer-Moore theorem prover","author":"Kaufmann","year":"1988","journal-title":"Technical Report 19, Computational Logic Inc."},{"issue":"4","key":"10.1016\/B978-044450813-3\/50015-1_bb0230","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1109\/32.588534","article-title":"An industrial strength theorem prover for a logic based on common lisp","volume":"23","author":"Kaufmann","year":"1997","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0235","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1112\/blms\/14.4.285","article-title":"Accessible independence results for Peano Arithmetic","volume":"14","author":"Kirby","year":"1982","journal-title":"Bull. London Math. Soc."},{"key":"10.1016\/B978-044450813-3\/50015-1_rf0240","series-title":"Automated Deduction - A Basis for Applications, Vol. II Systems and Implementation Techniques","first-page":"189","article-title":"Proof analysis, generalization and reuse","volume":"vol. 9","author":"Kolbe","year":"1998"},{"issue":"1-2","key":"10.1016\/B978-044450813-3\/50015-1_bb0245","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/BF00244461","article-title":"Middle-out reasoning for synthesis and induction","volume":"16","author":"Kraan","year":"1996","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0250","first-page":"95","article-title":"Mathematical logic","volume":"Vol. 3","author":"Kreisel","year":"1965"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0255","series-title":"The use of proof planning for co-operative theorem proving","author":"Lowe","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0260","series-title":"14th International Conference on Automated Deduction","first-page":"404","article-title":"XBarnacle: Making theorem provers more accessible","author":"Lowe","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0265","series-title":"6th International Congress for Logic, Methodology and Philosophy of Science","first-page":"153","article-title":"Constructive mathematics and computer programming","author":"Martin-L\u00f6f","year":"1979"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0270","series-title":"5th International Conference on Logic Programming and Automated Reasoning, LPAR'94","first-page":"54","article-title":"Proof Plans for the Correction of False Conjectures","volume":"v. 822","author":"Monroy","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0275","article-title":"Computational Logic: Structure sharing and proof of program properties, part II","author":"Moore","year":"1974","journal-title":"PhD thesis, University of Edinburgh"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0280","series-title":"ACM Transactions on Programming Languages and Systems","first-page":"245","article-title":"Simplification by cooperating decision procedures","author":"Nelson","year":"1979"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50015-1_bb0285","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-044450813-3\/50015-1_rf0290","series-title":"Sprawozdanie z I Kongresu metematyk\u00f3w slowia\u0144skich","first-page":"92","article-title":"\u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt","author":"Presburger","year":"1930"},{"key":"10.1016\/B978-044450813-3\/50015-1_rf0295","series-title":"Sprawozdanie z I Kongresu metematyk\u00f3w slowia\u0144skich","article-title":"\u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt","author":"Presburger","year":"1930"},{"key":"10.1016\/B978-044450813-3\/50015-1_rf0300","series-title":"Technical Report TR 84-639, Department of Computer Science, Cornell University","first-page":"395","article-title":"Presburger's article on integer arithmetic: Remarks and translation","author":"Stansifer","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0295","series-title":"11th International Conference on Automated Deduction","first-page":"340","article-title":"Disproving conjectures","author":"Protzen","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0300","series-title":"12th International Conference on Automated Deduction","first-page":"42","article-title":"Lazy generation of induction hypotheses","volume":"Vol. 814","author":"Protzen","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0305","series-title":"13th International Conference on Automated Deduction","first-page":"121","article-title":"Termination of algorithms over non-freely generated datatypes","author":"Sengler","year":"1996"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50015-1_bb0310","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-044450813-3\/50015-1_bb0315","article-title":"Presburger's article on integer arithmetic: Remarks and translation","author":"Stansifer","year":"1984","journal-title":"Technical Report TR 84-639, Department of Computer Science, Cornell University"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0320","series-title":"\u2018The Proceedings of ECAI-88', European Conference on Artificial Intelligence","first-page":"565","article-title":"A rational reconstruction of Boyer & Moore's technique for constructing induction formulas","author":"Stevens","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50015-1_rf0335","series-title":"Proceedings of the London Mathematical Society (2)","first-page":"230","article-title":"On computable numbers, with an application to the Entscheidungsproblem","author":"Turing","year":"1936"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0330","series-title":"International Conference on Logic Programming and Automated Reasoning \u2013 LPAR 92","article-title":"Computing induction axioms","author":"Walther","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0335","series-title":"\u2018Proceedings of IJCAI-93', International Joint Conference on Artificial Intelligence","first-page":"95","article-title":"Combining induction axioms by machine","author":"Walther","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0340","first-page":"122","article-title":"Mathematical induction","volume":"Vol. 2","author":"Walther","year":"1994"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50015-1_bb0345","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/0004-3702(94)90063-9","article-title":"On proving termination of algorithms by machine","volume":"71","author":"Walther","year":"1994","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0350","series-title":"Proceedings of ECAI-94","first-page":"85","article-title":"Coloured rippling: An extension of a theorem proving heuristic","author":"Yoshida","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50015-1_bb0355","series-title":"9th International Conference on Automated Deduction","first-page":"162","article-title":"A mechanizable induction principle for equational specifications","author":"Zhang","year":"1988"}],"container-title":["Handbook of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500151?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500151?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,1,6]],"date-time":"2019-01-06T19:25:56Z","timestamp":1546802756000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780444508133500151"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9780444508133"],"references-count":73,"URL":"https:\/\/doi.org\/10.1016\/b978-044450813-3\/50015-1","relation":{},"subject":[],"published":{"date-parts":[[2001]]}}}