Now showing items 1-5 of 5
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 ...
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 ...
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 ...