English
 
User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Conference Paper

Termination Orderings for Rippling

MPS-Authors
/persons/resource/persons44075

Basin,  David A.
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons45692

Walsh,  Toby
Programming Logics, MPI for Informatics, Max Planck Society;

External Ressource
No external resources are shared
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available
Citation

Basin, D. A., & Walsh, T. (1994). Termination Orderings for Rippling. In A. Bundy (Ed.), Proceedings of the 12th International Conference On Automated Deduction (CADE-12) (pp. 466-483). Berlin, Germany: Springer.


Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-ADAA-E
Abstract
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.