Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Case-Analysis for Rippling and Inductive Proof
Authors: Moa Johansson ; Lucas Dixon ; Alan Bundy
Date: 2009
Publication Title:CSL
Publication Type:Conference Paper Publication Status:Submitted
We introduce a method to support case-analysis as a step within rippling. The method allows consideration of if-statements as well as case-analysis on datatypes. By locating the case-analysis as a step within rippling we maintain the termination of rippling. The work has been implemented in IsaPlanner by adapting the existing inductive proof method. We evaluate this extended prover on a large set of examples from Isabelle's theory library as well as problems 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 also identified. These highlight the need for advances in the treatment of assumptions during rippling and when conjecturing lemmas.
Links To Paper
1st Link
Bibtex format
author = { Moa Johansson and Lucas Dixon and Alan Bundy },
title = {Case-Analysis for Rippling and Inductive Proof},
book title = {CSL},
year = 2009,
url = {},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh