text: In this paper, we investigate the potential of the Boyer-Moore waterfall model for the automation of inductive proofs within a modern proof assistant. We analyze the basic concepts and methodology underlying this 30-year-old model and implement a new, fully integrated tool in the theorem prover HOL Light that can be invoked as a tactic. We also describe several extensions and enhancements to the model. These include the integration of existing HOL Light proof procedures and the addition of state-of-the-art generalization techniques into the waterfall. Various features, such as proof feedback and heuristics dealing with non-termination, that are needed to make this automated tool useful within our interactive setting are also discussed. Finally, we present a thorough evaluation of the approach using a set of 150 theorems, and discuss the effectiveness of our additions and relevance of the model in light of our results.
  @cite_3: Preface 1. An introduction to rippling 2. Varieties of rippling 3. Productive use of failure 4. A formal account of rippling 5. The scope and limitations of rippling 6. From rippling to a general methodology 7. Conclusions Appendix 1. An annotated calculus and a unification algorithm Appendix 2. Definitions of functions used in this book Bibliography Index.
summary: One of the main heuristic tools in Proof Planning is Rippling @cite_3 . Rippling gives a direction to the rewriting process. The idea is based on the observation that throughout the process, on each side of the equality being proved, there is an unchanging part (skeleton) and a changing part (wave-front). In principle the proof is guided towards rewrite rules that move the wave-front upwards in the syntax tree of the term. Rippling has proved to be a powerful heuristic for inductive proofs. However, there is still a possibility that the proof will block, thus requiring a patch'' or critic''. Critics include lemma speculations and generalizations, some of which can be produced automatically in the modern Proof Planning systems.