@inproceedings{Yoshida94,
AUTHOR = "Yoshida, Tetsuja and Alan Bundy and Ian Green and Toby Walsh and David Basin",
TITLE = "Coloured Rippling: An Extension of a Theorem Proving Heuristic",
BOOKTITLE = "ECAI-94",
PUBLISHER = "John Whiley and Sons",
YEAR = "1994",
ABSTRACT = {
Rippling is a type of rewriting developed in inductive theorem
proving for removing differences between terms; the induction
conclusion is annotated to mark its differences from the induction
hypothesis and rippling attempts to move these differences.  Until now
rippling has been primarily employed in proofs where there is a single
induction hypothesis.  This paper describes an implemented extension
to the Clam proof planning system to deal with theorems with
multiple hypotheses.  Such theorems arise, for instance, when
reasoning about data-structures like trees with multiple recursive
arguments. The essential idea is to colour the annotation, with each
colour corresponding to a different hypothesis.  The annotation of
rewrite rules used in rippling is similarly generalized so that rules
propagate colours through terms.  This annotation guides search so
that rewrite rules are only applied if they reduce the differences
between the conclusion and some of the hypotheses.  We have tested
this implementation on a number of problems, including two of
Bledsoe's challenge limit theorems.
},
}