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 ...
Become an O’Reilly member and get unlimited access to this title plus top books and audiobooks from O’Reilly and nearly 200 top publishers, thousands of courses curated by job role, 150+ live events each month,
and much more.
Read now
Unlock full access