MPI-I-94-209
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.
-
MPI-I-94-209.pdf
- Attachement: MPI-I-94-209.ps (238 KBytes); MPI-I-94-209.pdf (212 KBytes)
URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1994-209
BibTeX
@TECHREPORT{BasinWalsh-94-mpii209,
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},
}