|
Informatics Report Series
|
|
|
|
|
|
|
|
|
| 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
|
|
|
|
|
- Abstract:
-
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
- @InProceedings{EDI-INF-RR-1326,
- author = {
Moa Johansson
and Lucas Dixon
and Alan Bundy
},
- title = {Case-Analysis for Rippling and Inductive Proof},
- book title = {CSL},
- year = 2009,
- url = {http://dream.inf.ed.ac.uk/projects/isaplanner/papers/case-split-rippling-09.pdf},
- }
|
