TY - GEN
T1 - Coloured rippling: An extension of a theorem proving heuristic
AU - Yoshida,Tetsuya
AU - Bundy,Alan
AU - Green,Ian
AU - Walsh,Toby
AU - Basin,David
PY - 1994
Y1 - 1994
N2 - 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 extension to rippling
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.
AB - 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 extension to rippling
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.
M3 - Conference contribution
BT - Proceedings of the Eleventh European Conference on Artificial Intelligence, Amsterdam, The Netherlands, August 8-12, 1994
PB - John Wiley & Sons Inc.
ER -