Keywords (1)

Case-Analysis for Rippling and Inductive Proof

Case-Analysis for Rippling and Inductive Proof,10.1007/978-3-642-14052-5_21,Moa Johansson,Lucas Dixon,Alan Bundy

Case-Analysis for Rippling and Inductive Proof  
BibTex | RIS | RefWorks Download
Rippling is a heuristic used to guide rewriting and is typ- ically 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 contribu- tion 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 of rippling. 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 as well as problems from the inductive theorem proving literature. We find that this leads to a significant improvement in the coverage of induc- tive 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.
Published in 2010.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.