Show simple item record

Interactive Theorem Proving, Series: Lecture Notes in Computer Science

dc.contributor.authorBundy, Alanen
dc.contributor.authorDixon, Lucasen
dc.contributor.authorJohansson, Moaen
dc.contributor.editorKaufmann, Men
dc.contributor.editorPaulson, L.C.en
dc.date.accessioned2010-09-07T14:41:19Z
dc.date.available2010-09-07T14:41:19Z
dc.date.issued2010
dc.identifier.isbnNA
dc.identifier.urihttp://hdl.handle.net/1842/3717
dc.description.abstractRippling is a heuristic used to guide rewriting and is typically used for inductive theorem proving. We introduce a method to support case-analysis within rippling. Like earlier work, this allows goals containing if-statements to be proved automatically. The new contribution is that our method also supports case-analysis on datatypes. By locating the case-analysis as a step within rippling we also maintain the termination. The work has been implemented in IsaPlanner and used to extend the existing inductive proof method. We evaluate this extended prover on a large set of examples from Isabelle’s theory library and from the inductive theorem proving literature. We find that this leads to a significant improvement in the coverage of inductive theorem proving. The main limitations of the extended prover are identified, highlight the need for advances in the treatment of assumptions during rippling and when conjecturing lemmas.en
dc.publisherSpringeren
dc.subjectComputer Scienceen
dc.subjectRipplingen
dc.subjectInteractive Theorem Provingen
dc.titleCase-Analysis for Rippling and Inductive Proofen
dc.typeBook Chapteren
dc.identifier.doi10.1007/978-3-642-14052-5_21
rps.titleInteractive Theorem Proving, Series: Lecture Notes in Computer Scienceen
dc.extent.pageNumbers291-306en
dc.date.updated2010-09-07T14:41:20Z


Files in this item

This item appears in the following Collection(s)

Show simple item record