Abstract
We show that theories presented by a set of ground equations with several associative-commutative (AC) symbols always admit a finite canonical system. This result is obtained through the construction of a reduction ordering which is AC-compatible and total on the set of congruence classes generated by the associativity and commutativity axioms. As far as we know, this is the first ordering with such properties, when several AC function symbols and free function symbols are allowed. Such an ordering is also a fundamental tool for deriving complete theorem proving strategies with built-in associative commutative unification.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
S. Anantharaman and J. Hsiang. An automated proof of the moufong identities in alternative rings. J. Automated Reasoning, 6:79–109, 1990.
L. Bachmair and N. Dershowitz. Commutation, transformation and termination. In J. Siekmann, editor, Proceedings 8th Conf. on Automated Deduction, pages 5–20, Springer-Verlag, 1986. Lecture Notes in Computer Science, volume 230.
L. Bachmair, N. Dershowitz, and J. Hsiang. Orderings for equational proofs. In Proceedings Symp. Logic in Computer Science, pages 346–357, Boston (Massachusetts USA), 1986.
A.M. Ballantyne and D. Lankford. New decision algorithms for finitely presented commutative semigroups. Comp. & Maths. with Appl., 7:159–165, 1981.
A. BenCherifa and P. Lescanne. Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming, 9(2):137–160, October 1987.
L. Bachmair and D.A. Plaisted. Termination orderings for associative-commutative rewriting systems. Journal of Symbolic Computation, 1:329–349, 1985.
N. Dershowitz. Termination of Rewriting. Journal of Symbolic Computation, 1 & 2:69–116, 1987.
N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In Van Leuven, editor, Handbook of Theoretical Computer Science, North Holland, 1990.
L. Dickson. Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. Amer. J. Math., XXXV:413–422, 1913.
J. Gallier, P. Narendran, D. Plaisted, S. Raatz, and W. Snyder. Finding canonical rewriting systems equivalent to a finite set of ground equations in polynomial time. In E. Lusk and R. Overbeek, editors, Proceedings 9th Int. Conf. on Automated Deduction, pages 182–196, Springer-Verlag, Lecture Notes in Computer Science, 1988.
J. Hsiang, and M. Rusinowitch. A new method for establishing refutational completeness in theorem proving. Proceedings of the 8th Conference on Automated Deduction, LNCS 230 (1986) 141–152.
G. Huet. Confluent reductions: abstract properties and applications to term rewriting systems. Journal of the Association for Computing Machinery, 27(4):797–821, October 1980.
J.-P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal of Computing, 15(4):1155–1194, 1986.
D. Kapur and P. Narendran. NP-completeness of the associative-commutative unification and related problems. Unpublished Manuscript, Computer Science Branch, General Electric Corporate Research and Development, Schenectady, NY, Dec. 1986.
D. Kapur and P. Narendran. A finite Thue system with decidable word problem and without equivalent finite canonical system. Theoretical Computer Science, 35:337–344, 1985.
D. Kapur, G. Sivakumar, and H. Zhang. A New Method for Proving Termination of AC-Rewrite Systems. To be presented at the Conference on the Foundations of Software Technology and Theoretical Computer Science, New Delhi, India, December 1990.
D.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, 1970.
D.S. Lankford. On Proving Term Rewriting Systems are Noetherian. Technical Report, Louisiana Tech. University, Mathematics Dept., Ruston LA, 1979.
D.S. Lankford and A. Ballantyne. Decision procedures for simple equational theories with permutative axioms: complete sets of permutative reductions. Technical Report, Univ. of Texas at Austin, Dept. of Mathematics and Computer Science, 1977.
E. W. Mayr. An algorithm for the general petri net reachability problem. In Proceedings of STOC, 1981.
P. Narendran and M. Rusinowitch. Unifiability in ground AC theories. 1990. In preparation.
G. Peterson and M. Stickel. Complete sets of reductions for some equational theories. Journal of the Association for Computing Machinery, 28:233–264, 1981.
W. Snyder. Efficient completion: an O(nlogn) algorithm for generating reduced sets of ground rewrite rules equivalent to a set of ground equations E. In N. Dershowitz, editor, Proceedings 3rd Conf. on Rewriting Techniques and Applications, pages —, Springer-Verlag, Lecture Notes in Computer Science, 1989.
Steinbach, J. AC-termination of rewrite systems — A modified Knuth-Bendix ordering. Proceedings 2nd International Conference on Algebraic and Logic Programming, Nancy (France), Lecture Notes in Computer Science 463, 372–386, (1990).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Narendran, P., Rusinowitch, M. (1991). Any ground associative-commutative theory has a finite canonical system. In: Book, R.V. (eds) Rewriting Techniques and Applications. RTA 1991. Lecture Notes in Computer Science, vol 488. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53904-2_115
Download citation
DOI: https://doi.org/10.1007/3-540-53904-2_115
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53904-9
Online ISBN: 978-3-540-46383-2
eBook Packages: Springer Book Archive