Now showing items 1-6 of 6
Case-Analysis for Rippling and Inductive Proof
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 ...
Formalising Term Synthesis for Isacosy
IsaCoSy is a theory formation system for inductive theories. It synthesises conjectures and uses the ones that can be proved to produce a background theory for a new formalisation within a proof assistant. We present a ...
Conjecture Synthesis for Inductive Theories
We have developed a program for inductive theory formation, called IsaCoSy, which synthesises conjectures ‘bottom-up’ from the available constants and free variables. The synthesis process is made tractable by only generating ...
Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery
We present a succinct account of dynamic rippling, a technique used to guide the automation of inductive proofs. This simplifies termination proofs for rippling and hence facilitates extending the technique in ways that ...
Isacosy: Synthesis of Inductive Theorems
We have implemented a program for inductive theory formation, called IsaCoSy, which synthesises conjectures about recursively deﬁned datatypes and functions. Only irreducible terms are generated, which keeps the search ...
Automated discovery of inductive lemmas
(The University of Edinburgh, 2009)
The discovery of unknown lemmas, case-splits and other so called eureka steps are challenging problems for automated theorem proving and have generally been assumed to require user intervention. This thesis is mainly ...