Original language | English |
---|
Title of host publication | Verification, Induction, Termination Analysis |
---|
Subtitle of host publication | Festschrift for Christoph Walther on the Occasion of His 60th Birthday |
---|
Editors | Simon Siegler, Nathan Wasser |
---|
Publisher | Springer-Verlag |
---|
Pages | 102-116 |
---|
Number of pages | 15 |
---|
Volume | 6463 |
---|
ISBN (Electronic) | 978-3-642-17172-7 |
---|
ISBN (Print) | 978-3-642-17171-0 |
---|
DOIs | |
---|
Publication status | Published - 2010 |
---|
Name | Lecture Notes in Computer Science |
---|
Publisher | Springer Berlin Heidelberg |
---|
Volume | 6463 |
---|
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