Termination Orderings for Rippling

Basin, David A.; Walsh, Toby

doi:10.1007/3-540-58156-1_34

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

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 Resource

https://rdcu.be/dtn8e
(Publisher version)

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

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: https://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.