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...
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...
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 ...