Catalogue of Artificial Intelligence Techniques
View Maths as: Images | MathML
Rippling
Keywords: heuristic, induction, proof-planning, rewriting, rippling
Categories: Theorem Proving
Author(s): Moa Johansson
Rippling is a heuristic used in automated theorem proving for reducing the differences between formulae. It was originally designed for inductive proofs, where the aim is to rewrite the inductive conclusion in such a way that the inductive hypothesis can be applied to advance the proof. Only rewrites that reduce differences and keep similarities are allowed. Rewrite rules can be applied both ways around and termination is guaranteed by defining a ripple measure that is required to decrease for each step of rewriting.
References:
- A. Bundy, D. Basin, D. Hutter and A. Ireland, Rippling: Meta-level Guidance for Mathematical Reasoning, Cambridge University Press, 2005.
Comments:
No comments.