Abstract
Rippling is a special type of rewriting developed for inductive theorem proving. Bundy 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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
D. Basin and T. Walsh. Difference unification. In Proceedings of the 13th IJCAI. International Joint Conference on Artificial Intelligence, 1993.
R.S. Boyer and J S. Moore. A Computational Logic. Academic Press, 1979. ACM monograph series.
A. Bundy, A. Stevens, F. van Harmelen, A. Ireland, and A. Smaill. Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence, 62:185–253, 1993.
A. Bundy, F. van Harmelen, C. Horn, and A. Smaill. The Oyster-Clam system. In M.E. Stickel, editor, 10th International Conference on Automated Deduction. 1990.
A. Bundy, F. van Harmelen, A. Smaill, and A. Ireland. Extensions to the rippling-out tactic for guiding inductive proofs. In M.E. Stickel, editor, 10th International Conference on Automated Deduction, pages 132–146. Springer-Verlag, 1990.
A. Bundy and B. Welham. Using meta-level inference for selective application of multiple rewrite rules in algebraic manipulation. Artificial Intelligence, 16(2):189–212, 1981.
N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17(3):279–301, March 1982.
N. Dershowitz. Termination of Rewriting. In J.-P. Jouannaud, editor, Rewriting Techniques and Applications.Academic Press, 1987.
N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B. North-Holland, 1990.
N. Dershowitz and Z. Manna. Proving termination with multiset orderings. Comms. ACM, 22(8):465–476, 1979.
D. Hutter. Guiding inductive proofs. In M.E. Stickel, editor, 10th International Conference on Automated Deduction. 1990.
D. Hutter. Colouring terms to control equational reasoning. An Expanded Version of PhD Thesis: Mustergesteuerte Strategien für Beweisen von Gleichheiten (Universität Karlsruhe, 1991), in preparation.
A. Ireland and A. Bundy. Using failure to guide inductive proof. Technical report, Dept. of Artificial Intelligence, University of Edinburgh, 1992.
T. Walsh, A. Nunes, and A. Bundy. The use of proof plans to sum series. In D. Kapur, editor, 11th Conference on Automated Deduction. 1992.
T. Yoshida, A. Bundy, I. Green, T. Walsh, and D. Basin. Coloured rippling: the extension of a theorem proving heuristic. Technical Report, Dept. of Artificial Intelligence, University of Edinburgh, 1993. Under review for ECAI-94.
Author information
Authors and Affiliations
Corresponding author
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Basin, D.A., Walsh, T. (1994). Termination orderings for rippling. In: Bundy, A. (eds) Automated Deduction — CADE-12. CADE 1994. Lecture Notes in Computer Science, vol 814. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58156-1_34
Download citation
DOI: https://doi.org/10.1007/3-540-58156-1_34
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58156-7
Online ISBN: 978-3-540-48467-7
eBook Packages: Springer Book Archive