Edinburgh Research Explorer

Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery

Research output: Chapter in Book/Report/Conference proceedingChapter

Original languageEnglish
Title of host publicationVerification, Induction, Termination Analysis
Subtitle of host publicationFestschrift for Christoph Walther on the Occasion of His 60th Birthday
EditorsSimon Siegler, Nathan Wasser
Number of pages15
ISBN (Electronic)978-3-642-17172-7
ISBN (Print)978-3-642-17171-0
StatePublished - 2010

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743


We present a succinct account of dynamic rippling, a technique used to guide the automation of inductive proofs. This simplifies termination proofs for rippling and hence facilitates extending the technique in ways that preserve termination. We illustrate this by extending rippling with a terminating version of middle-out reasoning for lemma speculation. This supports automatic speculation of schematic lemmas which are incrementally instantiated by unification as the rippling proof progresses. Middle-out reasoning and lemma speculation have been implemented in higher-order logic and evaluated on typical libraries of formalised mathematics. This reveals that, when applied, the technique often finds the needed lemmas to complete the proof, but it is not as frequently applicable as initially expected. In comparison, we show that theory formation methods, combined with simpler proof methods, offer an effective alternative.

ID: 142450