Handbook of Automated Reasoning

7 Rippling

Rippling is a difference reduction technique developed for induction proofs. It provides a partial solution to many of the special search control problems described in Section 6, page 865 above. Aubin was the first to notice a common pattern in the rewriting of step cases, [Aubin 1976]. In [Bundy 1988] it was proposed to use this pattern to drive the rewriting process and implementations of this proposal were first reported in [Bundy, van Harmelen, Smaill and Ireland 1990, Stevens, Ireland and Smaill 1993, Hutter 1990].

7.1 Rippling Out

Aubin observed that during the step case the differences between the induction conclusion and the induction hypothesis ripple-out of the induction conclusion, leaving a complete copy of the induction ...