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.
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.
@cite_3
1992696924
We present techniques to prove termination and innermost termination of term rewriting systems automatically. In contrast to previous approaches, we do not compare left- and right-hand sides of rewrite rules, but introduce the notion of dependency pairs to compare left-hand sides with special subterms of the right-hand sides. This results in a technique which allows to apply existing methods for automated termination proofs to term rewriting systems where they failed up to now. In particular, there are numerous term rewriting systems where a direct termination proof with simplification orderings is not possible, but in combination with our technique, well-known simplification orderings (such as the recursive path ordering, polynomial orderings, or the KnuthBendix ordering) can now be used to prove termination automatically. Unlike previous methods, our technique for proving innermost termination automatically can also be applied to prove innermost termination of term rewriting systems that are not terminating. Moreover, as innermost termination implies termination for certain classes of term rewriting systems, this technique can also be used for termination proofs of such systems.