Show simple item record

Induction, Verification and Termination Analysis

dc.contributor.authorJohansson, Moa
dc.contributor.authorDixon, Lucas
dc.contributor.authorBundy, Alan
dc.contributor.editorSiegler, Simon
dc.contributor.editorWasser, Nathan
dc.date.accessioned2011-02-03T11:21:22Z
dc.date.available2011-02-03T11:21:22Z
dc.date.issued2010
dc.identifier.isbn978-3-642-17171-0en
dc.identifier.urihttp://www.springerlink.com/content/v522k48032q1/#section=802652&page=1&locus=0en
dc.identifier.urihttp://hdl.handle.net/1842/4770
dc.description.abstractWe 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.en
dc.language.isoenen
dc.publisherSpringer-Verlagen
dc.titleDynamic Rippling, Middle-Out Reasoning and Lemma Discoveryen
dc.typeBook Chapteren
dc.identifier.doi1007/978-3-642-17172-7en
rps.volume6463 of LNAIen
rps.titleInduction, Verification and Termination Analysisen
dc.extent.pageNumbers102–116en
dc.date.updated2011-02-03T11:21:22Z


Files in this item

This item appears in the following Collection(s)

Show simple item record