Sciweavers

BIRTHDAY
2010
Springer
13 years 7 months ago
Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery
Abstract. 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...
Moa Johansson, Lucas Dixon, Alan Bundy
BIRTHDAY
2006
Springer
13 years 10 months ago
Best-First Rippling
Rippling is a form of rewriting that guides search by only performing steps that reduce the syntactic differences between formulae. Termination is normally ensured by a measure th...
Moa Johansson, Alan Bundy, Lucas Dixon
ITP
2010
140views Mathematics» more  ITP 2010»
13 years 10 months ago
Case-Analysis for Rippling and Inductive Proof
Abstract. 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 ...
Moa Johansson, Lucas Dixon, Alan Bundy