Extension of the associative path ordering to a chain of associative commutative symbols
In this paper, we give a generalization of the associative path ordering. This ordering has been introduced by Bachmair and Plaisted  and is a restricted variant of the recursive path ordering which can be used for proving the termination of associative-commutative term rewriting systems. This ordering requires strong conditions on the precedence on the alphabet. In this article, we treat the case of a precedence which contains a chain of AC symbols. We also introduce some unary symbols comparable with AC symbols.
KeywordsNormal Form Commutative Ring Normalization System Normalization Rule Distributivity Rule
Unable to display preview. Download preview PDF.
- 1.Leo Bachmair. Proof Methods for Equational Theories. PhD thesis, University of Illinois at Urbana-Champaign, 1987.Google Scholar
- 2.Leo Bachmair. Associative-commutative reduction orderings. Info Proc. Letters, 1992.Google Scholar
- 3.Leo Bachmair and Nachum Dershowitz. Commutation, transformation, and termination. In Jorg H. Siekmann, editor, Proc. 8th Int. Conf. on Automated Deduction, Oxford, England, LNCS 230, pages 5–20, July 1986.Google Scholar
- 4.Leo Bachmair and Nachum Dershowitz. Completion for rewriting modulo a congruence. In Pierre Lescanne, editor, Proceedings of the Second International Conference on Rewriting Techniques and Applications, pages 192–203, Bordeaux, France, May 1987. Vol. 256 of Lecture Notes in Computer Science, Springer, Berlin.Google Scholar
- 6.Ahlem Ben Cherifa and Pierre Lescanne. Termination of rewriting systems by polynomial interpretations and its implementation. Research Report 677, INRIA, June 1987.Google Scholar
- 7.Hubert Comon and Catherine Delor. Equational formulas with membership constraints. Technical report, Laboratoire de Recherche en informatique, March 1991. To appear in Information and Computation.Google Scholar
- 8.Paliath Narendran and MichaÃ«l Rusinowitch. Any ground associative-commutative theory has a finite canonical system. In Ronald V. Book, editor, Proc. 4th Rewriting Techniques and Applications, Como, LNCS 488. Springer-Verlag, April 1991.Google Scholar
- 9.Joachim Steinbach. AC-termination of rewrite systems: a modified Knuth-Bendix ordering. In H. Kirchner and W. Wechler, editors, Proc. 2nd Int. Conf. on Algebraic and Logic Programming, LNCS 463, pages 372–386, October 1990.Google Scholar
- 10.Joachim Steinbach. Improving associative path orderings. In Proc. 10th Int. Conf. on Automated Deduction, Kaiserslautern, LNCS 449. Springer-Verlag, July 1990.Google Scholar