MPI-INF/SWS Research Reports 1991-2017

2. Number - only D2


Termination orderings for rippling

Basin, David A. and Walsh, Toby

February 1994, 15 pages.

Status: available - back from printing

Rippling is a special type of rewriting developed for inductive theorem proving. Bundy {\em 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 enlarging 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 rewriting. Such combinations offer the flexibility and uniformity of conventional rewriting with the highly goal directed nature of rippling. Finally, we show how our orders simplify implementation of provers based on rippling.

  • Attachement: (238 KBytes); MPI-I-94-209.pdf (212 KBytes)

URL to this document:

Hide details for BibTeXBibTeX
  AUTHOR = {Basin, David A. and Walsh, Toby},
  TITLE = {Termination orderings for rippling},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-94-209},
  MONTH = {February},
  YEAR = {1994},
  ISSN = {0946-011X},