Abstract
A graded sequence of examples—presented in a uniform framework—spotlights stages in the development of methods for proving termination of rewrite systems.
Research supported in part by the U. S. National Science Foundation under Grants CCR-90-07195 and CCR-90-24271.
Preview
Unable to display preview. Download preview PDF.
References
Nachum Dershowitz and Charles Hoot. Natural termination. Theoretical Computer Science, to appear.
Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, chapter 6, pages 243–320. North-Holland, Amsterdam, 1990.
Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465–476, August 1979.
Nachum Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17(3):279–301, March 1982.
Nachum Dershowitz. Termination of rewriting. J. Symbolic Computation, 3(1&2):69–115, February/April 1987. Corrigendum: 4, 3 (December 1987), 409–410; reprinted in Rewriting Techniques and Applications, J.-P. Jouannaud, ed., pp. 69–115, Academic Press, 1987.
Trevor Evans. On multiplicative systems defined by generators and relations, I. Proceedings of the Cambridge Philosophical Society, 47:637–649, 1951.
Saul Gorn. On the conclusive validation of symbol manipulation processes (how do you know it has to work?). J. of the Franklin Institute, 296(6):499–518, December 1973.
R. Iturriaga. Contributions to mechanical mathematics. Ph.D. Thesis, Department of Computer Science, Carnegie-Mellon University, Pittsburgh, PA, 1967.
Sam Kamin and Jean-Jacques LĂ©vy. Two generalizations of the recursive path ordering. Unpublished note, Department of Computer Science, University of Illinois, Urbana, IL, February 1980.
Jan Willem Klop. Term rewriting systems. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, chapter 1, pages 1–117. Oxford University Press, Oxford, 1992.
Donald E. Knuth and P. B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, Oxford, U. K., 1970. Reprinted in Automation of Reasoning 2, Springer-Verlag, Berlin, pp. 342–376 (1983).
Dallas S. Lankford. On proving term rewriting systems are Noetherian. Memo MTP-3, Mathematics Department, Louisiana Tech. University, Ruston, LA, May 1979. Revised October 1979.
R. Lipton and L. Snyder. On the halting of tree replacement systems. In Proceedings of the Conference on Theoretical Computer Science, pages 43–46, Waterloo, Canada, August 1977.
Zohar Manna and Steven Ness. On the termination of Markov algorithms. In Proceedings of the Third Hawaii International Conference on System Science, pages 789–792, Honolulu, HI, January 1970.
David A. Plaisted. Well-founded orderings for proving termination of systems of rewrite rules. Report R-78-932, Department of Computer Science, University of Illinois, Urbana, IL, July 1978.
David A. Plaisted. A recursively defined ordering for proving termination of term rewriting systems. Report R-78-943, Department of Computer Science, University of Illinois, Urbana, IL, September 1978.
David A. Plaisted. Term rewriting systems. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 4, chapter 2. Oxford University Press, Oxford, 1993. To appear.
Hans Zantema. Classifying termination of term rewriting. Technical Report RUU-CS-91-42, Utrecht University, The Netherlands, November 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dershowitz, N. (1995). 33 Examples of termination. In: Comon, H., Jounnaud, JP. (eds) Term Rewriting. TCS School 1993. Lecture Notes in Computer Science, vol 909. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59340-3_2
Download citation
DOI: https://doi.org/10.1007/3-540-59340-3_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59340-9
Online ISBN: 978-3-540-49237-5
eBook Packages: Springer Book Archive