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
PublisherSpringer-Verlag
Pages102-116
Number of pages15
Volume6463
ISBN (Electronic)978-3-642-17172-7
ISBN (Print)978-3-642-17171-0
DOIs
StatePublished - 2010

Publication series

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

Abstract

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