RIPPLING - A HEURISTIC FOR GUIDING INDUCTIVE PROOFS

We describe rippling: a tactic for the heuristic control of the key pa rt of proofs by mathematical induction. This tactic significantly redu ces the search for a proof of a wide variety of inductive theorems. We first present a basic version of rippling, followed by various extens ions which are necessary to capture larger classes of inductive proofs . Finally, we present a generalised form of rippling which embodies th ese extensions as special cases. We prove that generalised rippling al ways terminates, and we discuss the implementation of the tactic and i ts relation with other inductive proof search heuristics.