Abstract
We prove that a canonical set of rules for an equational theory defined by a finite set of ground axioms plus the associativity and commutativity of any number of operators must be finite.
As a corollary, we show that ground AC-completion, when using a total AC-simplification ordering and an appropriate control, must terminate.
Using a recent result of Narendran and Rusinowitch (in this volume), this implies that the word problem for such a theory is decidable.
This work is partly supported by the “GRECO de programmation du CNRS” and Basic Research Action COMPASS
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, N. Dershowitz, and J. Hsiang. Orderings for equational proofs. In Proc. 1st IEEE Symp. Logic in Computer Science, Cambridge, Mass., pages 346–357, June 1986.
N. Dershowitz and J.-P. Jouannaud. Handbook of Theoretical Computer Science, volume B, chapter Rewrite Systems, pages 243–309. North-Holland, 1990. J. van Leeuwen ed.
P. W. Goldberg. Ground AC-Completion. Laboratoire de Recherche en informatique, internal report, 1989.
G. Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, 2(3):326–336, Sept. 1952.
J.-P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM J. Comput., 15(4):1155–1194, 1986.
D. S. Lankford and A. M. Ballantyne. Decision procedures for simple equational theories with commutative-associative axioms: Complete sets of commutative-associative reductions. Research Report Memo ATP-39, Department of Mathematics and Computer Science, University of Texas, Austin, Texas, USA, Aug. 1977.
A. Mal'cev. On homomorphisms of finite groups. Ivano Gosudarstvenni Pedag. Inst. Ucheneye Zap, 18:49–90, 1958.
C. Marché. On AC-termination and ground AC-completion. Research Report 598, Laboratoire de Recherche en Informatique, Université de Paris-Sud, Orsay, France, Oct. 1990.
A. A. Markov. On the impossibility of certain algorithms in the theory of associative systems. Dokl. Akad. Nauk SSSR, 55:587–590, 1947. In Russian, English translation in C.R. Acad. Sci. URSS, 55, 533–586.
J. V. Matijasevic. Simple examples of undecidable associative calculi. Soviet Mathematics (Dokladi), 8(2):555–557, 1967.
G. E. Peterson and M. E. Stickel. Complete sets of reductions for some equational theories. J. ACM, 28(2):233–264, Apr. 1981.
E. L. Post. Recursive unsolvability of a problem of Thue. Journal of Symbolic Logic, 12:1–11, 1947.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Marché, C. (1991). On ground AC-completion. 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_114
Download citation
DOI: https://doi.org/10.1007/3-540-53904-2_114
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