In computer science, more particularly in automated theorem proving, rippling[1] refers to a group of meta-level heuristics, developed primarily in the Mathematical Reasoning Group in the School of Informatics at the University of Edinburgh, and most commonly used to guide inductive proofs in automated theorem proving systems.
Raymond Aubin was the first person to use the term "rippling out" whilst working on his 1976 PhD thesis[2] at the University of Edinburgh.
Alan Bundy later turned this concept on its head by defining rippling to be this pattern of movement, rather than a side effect.
Rippling has been applied to many problems traditionally viewed as being hard in the inductive theorem proving community, including Bledsoe's limit theorems[citation needed] and a proof of the Gordon microprocessor,[citation needed] a miniature computer developed by Michael J. C. Gordon and his team at Cambridge.
Note that the final rewrite causes all wave-fronts to disappear, and we may now apply fertilization, the application of the inductive hypotheses, to complete the proof.