Edinburgh Research Explorer

Case-Analysis for Rippling and Inductive Proof

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Related Edinburgh Organisations

Access status

Open

Original languageEnglish
Title of host publicationInteractive Theorem Proving, Series
Subtitle of host publicationFirst International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings
EditorsM. Kaufmann, L. C. Paulson
PublisherSpringer-Verlag GmbH
Pages291-306
Number of pages16
ISBN (Electronic)978-3-642-14052-5
ISBN (Print)978-3-642-14051-8
DOIs
StatePublished - 2010

Publication series

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

Abstract

Rippling 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.

Research areas

  • Computer Science, Rippling, Interactive Theorem Proving

Download statistics

No data available

ID: 142468