Abstract
We propose in this paper a special reduction ordering for proving termination of Associative Commutative (AC in short) rewriting systems. This ordering is based on a transformation of the terms by a rewriting system with rules similar to distributivity. We show this is a reduction ordering which works in the AC case since it is AC-commuting, and which provides an automatizable termination tool, since it is stable by instantiation. Thereafter, we show cases where this ordering fails, and propose an extension of this method to other transformation rules such as endomorphism.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
L. Bachmair and D. Plaisted, ”Associative Path Orderings,” in Proc. 1st Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 202, pp. 241–254, Springer Verlag, Dijon (France), 1985.
L. Bachmair and N. Dershowitz, ”Commutation, Transformation, and Termination,” Inter. Report U. of Illinois, 1985.
A. Ben Cherifa and P. Lescanne, ”An actual implementation of a procedure that mechanically proves termination of rewriting systems based on inequalities between polynomial interpretations,” in CADE, 1986.
Nachum Dershowitz, ”Orderings for Term-Rewriting Systems,” Theoretical Computer Science, vol. 17, pp. 279–301, 1982.
N. Dershowitz, ”Termination,” in Proc. 1rst Conf. Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 202, pp. 180–224, Springer Verlag, Dijon (France), May 1985.
I. Gnaedig, ”Preuves de Terminaison des Systemes de Reecriture Associatifscommutatifs: une Methode Fondee sur la Reecriture Elle-meme,” These de troisieme cycle, Nancy, 1986.
G. Huet and D. Oppen, ”Equations and Rewrite Rules: A Survey,” in Formal Languages: Perspectives And Open Problems, ed. Book R., Academic Press, 1980.
J.P. Jouannaud and M. Munõz, ”Termination of a set of rules modulo a set of equations,” Proceedings 7th Conference on Automated Deduction, vol. 170, Napa Valley (California, USA), 1984.
D. Knuth and P. Bendix, ”Simple Word Problems in Universal Algebras,” Computational Problems in Abstract Algebra Ed. Leech J., Pergamon Press, pp. 263–297, 1970.
D.S. Lankford, ”On Proving Term Rewriting Systems Are Noetherian,” Report Mtp-3, Math. Dept., Louisiana Tech University, May 1979.
M. Munõz, ”Probleme de terminaison finie des systemes de reecriture equationnels,” These 3eme Cycle, Universite de Nancy 1, 1984.
D.A. Plaisted, ”An associative path ordering,” in Proc. NSF Workshop on the Rewrite Rule Laboratory, pp. 123–136, General Electric, Schenectady, New-York, April 1984.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gnaedig, I., Lescanne, P. (1986). Proving termination of associative commutative rewriting systems by rewriting. In: Siekmann, J.H. (eds) 8th International Conference on Automated Deduction. CADE 1986. Lecture Notes in Computer Science, vol 230. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16780-3_79
Download citation
DOI: https://doi.org/10.1007/3-540-16780-3_79
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16780-8
Online ISBN: 978-3-540-39861-5
eBook Packages: Springer Book Archive