O'Reilly logo

Handbook of Automated Reasoning by Andrei Voronkov, Alan J.A. Robinson

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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 ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required