MRG home page · Research · Publications · Projects · Software · People

Case-Analysis Results

The case-analysis evaluation corpus consists of 87 theorems about functions defined using conditional statements over natural numbers, lists and binary trees. IsaPlanner's rippling technique can automatically prove 47 of these theorems, only using the function definitions and not supplied with any extra lemmas. A simpler technique, applying induction followed by Isabelle's simplifier proves 37 theorems. We also experimented with a modification to our original case-analysis technique for rippling, allowing it to conjecture non-rippling goals after case-splitting as lemmas. This technique was able to prove 49 theorems, but would often not terminate on theorems it could not solve, which does not happen for the standard version.

The Isabelle theory files used in the experiments are below:

Webpage maintained by Moa Johansson
Mathematical Reasoning Group, Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland
Tel: +44 (0)131 650 2733      Fax: +44 (0)131 650 6899
Please send corrections and suggestions for this page to the DReaM Support Team
Unless explicitly stated otherwise all material on this web site is copyright © The University of Edinburgh.