Abstract
Term rewriting systems provide a simple mechanism for computing in equations. An equation is converted into a directed rewrite rule by comparing both sides w.r.t. an ordering. However, there exist equations which are incomparable. The handling of such equations includes, for example, partitioning the given equational theory into a set R of rules and a set E of equations. The appropriate reduction relation allows reductions modulo the equations in E. The effective computation with this relation presumes E-termination. This report deals with a new ordering applicable to [R,E]-systems where E contains associative-commutative equations. The method is based on the Knuth-Bendix ordering and is AC-commuting, a property introduced by Jouannaud and Munoz.
This research was supported by the Deutsche Forschungsgemeinschaft, SFB314
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Ahlem Ben Cherifa / Pierre Lescanne: Termination of rewriting systems by polynomial interpretations and its implementation, Science of Computer Programming 9 [2], October 1987, pp. 137–160
Leo Bachmair / David A. Plaisted: Termination orderings for associative-commutative rewriting systems, Journal of Symbolic Computation 1, 1985, pp. 329–349
Max Dauchet: Termination of rewriting is undecidable in the one-rule case, Proc. 13th Symposium of Mathematical Foundations of Computer Science, Carlsbad, CSFR, September 1988, LNCS 324, pp. 262–270
Nachum Dershowitz: Termination of rewriting, Journal of Symbolic Computation 3, 1987, pp. 69–116
Nachum Dershowitz / Jieh Hsiang / N. Alan Josephson / David A. Plaisted: Associative-commutative rewriting, Proc. 8th International Joint Conference on Artificial Intelligence, Karlsruhe. W. Germany, August 1983, pp. 940–944
Bernhard Gramlich / Jörg Denzinger: Efficient AC-matching using constraint propagation, SEKI-Report SR-88-15, Univ. of Kaiserslautern, W. Germany, 1988
Isabelle Gnaedig / Pierre Lescanne: Proving termination of associative-commutative rewriting systems by rewriting, Proc. 8th Conference on Automated Deduction, Oxford, England 1986, LNCS 230, pp. 52–60
Isabelle Gnaedig: Investigations on termination of equational rewriting, Report INRIA, Le Chesnay, France, 1987
Isabelle Gnaedig: Total orderings for equational theories, Working document, Nancy, France, 1988
Jean-Pierre Jouannaud / Helene Kirchner: Completion of a set of rules modulo a set of equations, SIAM Journal on Computing 15 [4], November 1986, pp. 1155–1194
Jean-Pierre Jouannaud / Miguel Munoz: Termination of a set of rules modulo a set of equations, Proc. 7th Conference on Automated Deduction, Napa, California, 1984, LNCS 170, pp. 175–193
Donald E. Knuth / Peter B. Bendix: Simple word problems in universal algebras, Computational Problems in Abstract Algebra, Pergamon Press, 1970, pp. 263–297
Sam Kamin / Jean-Jacques Levy: Attempts for generalizing the recursive path orderings, Unpublished manuscript, Dept. of Computer Science, Univ. of Urbana, Illinois, February 1980
Dallas S. Lankford: Some approaches to equality for computational logic: A survey and assessment, Report ATP-36, Dept. of Mathematics and Computer Science, Univ. of Texas, Austin, Texas, Spring 1977
Dallas S. Lankford: On proving term rewriting systems are noetherian, Memo MTP-3, Mathematics Dept., Univ. of Ruston, Louisiana, May 1979
Dallas S. Lankford / A.M. Ballantyne: Decision procedures for simple equational theories with commutative-associative axioms: Complete sets of commutative-associative reductions, Report ATP-39, Dept. of Mathematics and Computer Science, Univ. of Texas, Austin, Texas, August 1977
Ursula Martin: How to choose the weights in the Knuth-Bendix ordering, Proc. 2nd International Conference on Rewriting Techniques and Applications, Bordeaux, France, May 1987, LNCS 256, pp. 42–53
David A. Plaisted: An associative path ordering, Proc. NFS Workshop on the RRL, Schenectady, New York, November 1983, pp. 123–136
Joachim Steinbach: Term orderings with status, SEKI-Report SR-88-12, Univ. of Kaiserslautern, W. Germany, 1988
Joachim Steinbach: Extensions and comparison of simplification orderings, Proc. 3rd International Conference on Rewriting Techniques and Applications, Chapel Hill, North Carolina, April 1989, LNCS 355, pp. 434–448
Joachim Steinbach: Proving termination of associative-commutative rewriting systems using the Knuth-Bendix ordering, SEKI-Report SR-89-13, Univ. of Kaiserslautern, W. Germany, 1989
Joachim Steinbach: Path and decomposition orderings for proving AC-termination, SEKI-Report SR-89-18, Univ. of Kaiserslautern, W. Germany, 1989
Joachim Steinbach: Associative-commutative Knuth-Bendix ordering, Proc. 2nd German Workshop “Term Rewriting: Theory and Applications”, Ganzinger et al. [eds.], Dortmund, W. Germany, March 1990, pp. 19–21
Joachim Steinbach: Improving associative path orderings, Proc. 10th Conference on Automated Deduction, Kaiserslautern, W. Germany, July 1990, to appear
Joachim Steinbach / Michael Zehnter: Vade-mecum of polynomial orderings, SEKI-Report SR-90-3, Univ. of Kaiserslautern, W. Germany, 1990
Michael Zehnter: Orderings modulo theories — A guide, Project Report, Univ. of Kaiserslautern, W. Germany, 1989 [in German]
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Steinbach, J. (1990). AC-Termination of rewrite systems: A modified Knuth-Bendix ordering. In: Kirchner, H., Wechler, W. (eds) Algebraic and Logic Programming. ALP 1990. Lecture Notes in Computer Science, vol 463. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53162-9_52
Download citation
DOI: https://doi.org/10.1007/3-540-53162-9_52
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53162-3
Online ISBN: 978-3-540-46738-0
eBook Packages: Springer Book Archive