@article{BasinWalsh96,
Author = "Basin, David and Toby Walsh",
Title = "A Calculus for and Termination of Rippling",
journal = "Journal of Automated Reasoning",
volume = 16,
number = "1--2",		  
pages = "147--180",
year = 1996,
ABSTRACT      = { 
Rippling is a  type of rewriting developed for inductive
theorem proving which uses annotations to direct search.
Rippling has many desirable properties: for example, it is
highly goal directed, usually involves little search, and always terminates.
In this paper we give a new and more general formalization of
rippling. We introduce a simple calculus for rewriting annotated terms,
close  in spirit to first-order rewriting, and prove that it
has the formal properties desired of rippling.   Next we develop criteria
for proving the termination of such annotated rewriting,
and introduce orders on annotated terms that lead to termination.
In addition, we show how
to make rippling more flexible by adapting the termination orders
to the problem domain.  Our work has practical as well
as theoretical advantages: it has led to
a very simple implementation of rippling
that has been integrated in the Edinburgh CLAM system.  },
}