My impression is that the article falls apart into the individual contributions of the two authors which aim at different goals. J's part is a history of the (early) Boyer/Moore provers and it's interesting to see how they developed over the time (Chapters 1,2,5). Most of the article is devoted to their early provers Pure LISP Theorem Prover and THM (more than 30 pages). It illustrates nicely the techniques and the evolution of these tools. The drawback is that this chapter on explicit induction depicts *only* (well, except one single page) work of B&M. The history of automated induction (based on explict induction) is the history of Boyer & Moore in the 70s: "In this context, it is surprising that for the field of quantifier- free first-order inductive theorem proving based on recursive functions, most of the progress toward general usefulness took place within the 1970s and that usefulness was clearly demonstrated by 1986. In this article we describe how this giant step took place, and sketch the further development of automated inductive theorem proving." (page 2) and "Contrary to the excellent handbook articles..., our focus in this article is neither on current standards, nor on the engineering and research problems of the field, but on the history of the automation of mathematical induction." (page 5). The justification for this is given in Section 5.3.9 "Restricted to the mechanization of explicit induction no significant progress has been seen beyond THM..." (which was finished in the 70s). This sentence is both, true and false and it's also provocative. It's true in a sense that "explicit induction" is far more than only the selection of an appropriate schema but also the corresponding rewriting / deduction of both, the base case and induction step as well as lemma generation / generalization in case of failure. A main contribution of B&M was to identify these individual issues and to orchestrate solutions for the individual issues to a powerful tool (based the "waterfall"). But the sentence above is also false since in the 90s significant improvements have been gained in automating / tuning such techniques (e.g. termination analysis, rewriting). While explicit induction was basically finished in 1986, other approaches - according to the other author - using implicit orderings didn't work from the start: "The entire handbook article [Comon, 2001] (with corrections in [Wirth, 2005a]) is dedicated to the two aspects of proof by consistency and implicit induction orderings. Today, however, the interest in these two aspects tends to be historical or theoretical, especially because these aspects can hardly be combined with explicit induction." Given this explicite focus on the history / early work of B&M, Chapters 3, 4 6 don't really fit into that story. Chapter 3 and 4 (induction / recursion) are not mainly concerned with the history / development of induction / recursion schemes over the time to support automation but provide scholarly work on defining induction schemes/axioms in general. It would have beem nice to see this basis applied in the later Chapter 5. It would have been also a good opportunity to discuss the alternatives of syntactic vs. semantic based orderings in these chapters and how they have been influenced each others (e.g. Basin's article). Chapter 6 (and 5.6) is just some sort of name-dropping of all the other developments concerning the automation of induction but doesn't fit to the description of B&M provers neither in length nor in its thoroughness/ details (which would be also impossible wrt. the overall length restrictions of such an article). BTW, I don't understand why Rippling is "besides explicit induction" as it is developed as a strategy to guide the proof of induction steps using explicit induction. Also many claims (mostly wrt. inductionless induction) are made in Chapter 6 which are not backed up by a substantial scholar argumentation. Summing up, I have some difficulties with the article since it is not well balanced given the rather general title. It comprises some nice aspects wrt. the *history* of Boyer-Moore theorem provers and some nice *scholar* aspects wrt. the induction by Descente Infinie. But both parts do not fit together very nicely. Reading about the history of automated induction I would have loved to see the different competing approaches and the decisions "evolution" made in the past. In past CADEs, workshops etc. there were a lot of discussions about such competing approaches, like - typed vs. untyped calculi - explicit vs. implicit induction - first-order + induction schemes vs. higher-order calculi - symbolic evaluation vs. rippling vs. other search strategies - fixing induction schemes at the beginning vs. "lazy" induction" - programming languages vs. resolution style representation - which decisions have to be made at which steps to restrict search space? and many more... Unfortunately, these bits have not been seriously tackled by the article. After some years of rather low interest, research in induction is improving in the last years. Reading this article, what lessons can researcher being active in this field now learn to build their own inductive theorem provers? ---- Might be interesting: the outline of the article: 1 A SNAPSHOT OF A DECISIVE MOMENT IN HISTORY (4) 1 2 METHOD OF PROCEDURE AND PRESENTATION (4) 5 2.1 Organization of This Article 8 3 MATHEMATICAL INDUCTION (19) 9 3.1 Well-foundedness and Termination 10 3.2 The Theorem of Noetherian Induction 10 3.3 An Induction Principle Stronger Than Noetherian Induction? 11 3.4 The Natural Numbers 12 3.5 Standard Data Types 15 3.6 The Standard High-Level Method of Mathematical Induction 18 3.7 Descente Infinie 19 3.8 Explicit Induction 22 3.9 Generalization 26 3.10 Proof-Theoretical Peculiarities of Mathematical Induction 28 3.11 Conclusion 28 4 RECURSION AND TERMINATION (10) 29 4.1 Confluence 29 4.2 Termination and Reducibility 31 4.3 Constructor Variables 31 4.4 Termination and General Induction Templates 33 4.5 Termination of the Rewrite Relation on Ground Terms 35 4.6 Applicable Induction Templates for Explicit Induction 35 4.7 Induction Schemes 36 5 AUTOMATED EXPLICIT INDUCTION (38) 39 5.1 The Application Context of Automated Explicit Induction 39 5.2 The Pure LISP Theorem Prover 40 5.3 Thm 50 5.4 Nqthm 72 5.5 ACL2 73 5.6 Explicit Induction in Rrl, Inka, and Oyster/CLaM 75 6 ALTERNATIVE APPROACHES BESIDES EXPLICIT INDUCTION (5) 77 6.1 Proof Planning 77 6.2 Rippling 77 6.3 Implicit Induction 78 6.4 QuodLibet 80 7 LESSONS LEARNED (1) 82 8 CONCLUSION 83