Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


Termination orderings for rippling

Basin, David A. and Walsh, Toby

MPI-I-94-209. February 1994, 15 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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.
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-94-209.pdfMPI-I-94-209.pdfMPI-I-94-209.ps238 KBytes; 212 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
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},