Extension of the associative path ordering to a chain of associative commutative symbols

  • Catherine Delor
  • Laurence Puel
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 690)


In this paper, we give a generalization of the associative path ordering. This ordering has been introduced by Bachmair and Plaisted [5] 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.


Normal Form Commutative Ring Normalization System Normalization Rule Distributivity Rule 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Leo Bachmair. Proof Methods for Equational Theories. PhD thesis, University of Illinois at Urbana-Champaign, 1987.Google Scholar
  2. 2.
    Leo Bachmair. Associative-commutative reduction orderings. Info Proc. Letters, 1992.Google Scholar
  3. 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. 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
  5. 5.
    Leo Bachmair and David A. Plaisted. Termination orderings for associative-commutative rewriting systems. Journal of Symbolic Computation, 1(4):329–349, December 1985.CrossRefMATHMathSciNetGoogle Scholar
  6. 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. 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. 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. 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. 10.
    Joachim Steinbach. Improving associative path orderings. In Proc. 10th Int. Conf. on Automated Deduction, Kaiserslautern, LNCS 449. Springer-Verlag, July 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Catherine Delor
    • 1
  • Laurence Puel
    • 1
  1. 1.Laboratoire de Recherche en Informatique Bat.490Université de Paris SudOrsay CedexFrance

Personalised recommendations