Catalogue of Artificial Intelligence Techniques


Jump to: Top | Entry | References | Comments

View Maths as: Images | MathML


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.



Add Comment

No comments.