TY - GEN
T1 - Case-Analysis for Rippling and Inductive Proof
AU - Johansson, Moa
AU - Dixon, Lucas
AU - Bundy, Alan
PY - 2010
Y1 - 2010
N2 - 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.
AB - 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.
KW - Computer Science
KW - Rippling
KW - Interactive Theorem Proving
U2 - 10.1007/978-3-642-14052-5_21
DO - 10.1007/978-3-642-14052-5_21
M3 - Conference contribution
SN - 978-3-642-14051-8
T3 - Lecture Notes in Computer Science
SP - 291
EP - 306
BT - Interactive Theorem Proving, Series
A2 - Kaufmann, M.
A2 - Paulson, L. C.
PB - Springer-Verlag GmbH
ER -