Catalogue of Artificial Intelligence Techniques

   

Jump to: Top | Entry | References | Comments

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:


Comments:

Add Comment

No comments.