Termination Orderings for Rippling
David Basin, Toby Walsh · 1994
Abstract. Rippling is a special type of rewriting developed for induct-ive theorem proving. Bundy et. al. have shown that rippling terminates by providing a well-founded order for the annotated rewrite rules used by rippling. Here, we simplify and generalize this order, thereby enlar-ging the class of rewrite rules that can be used. In addition, we extend the power of rippling by proposing new domain dependent orders. These extensions elegantly combine rippling with more conventional term re-writing. Such combinations oer the exibility and uniformity of conven-tional rewriting with the highly goal directed nature of rippling. Finally, we show how our orders simplify implementation of provers based on rippling. 1