Abstract
We show that the \( \exists ^ * \forall ^ * \) part of the equational theory modulo an AC symbol is undecidable. This solves the open problem 25 from the RTA list ([DJK91],[DJK93],[DJK95])
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
H. Comon, Complete axiomatizations of some quotient term algebras Theoretical Computer Science, 118(2), September 1993
N. Dershowitz, J-P Jouannaud, J. W. Klop, Problems in Rewriting, Proceedings of 4 RTA, 1991, (Springer LNCS vol. 448), pp 445–456
N. Dershowitz, J-P Jouannaud, J. W. Klop, More Problems in Rewriting, Proceedings of 5th RTA, 1993, (Springer LNCS vol. 690) pp. 468–487
N. Dershowitz, J-P Jouannaud, J. W. Klop, Problems in Rewriting III, Proceedings of RTA 95, (Springer LNCS vol. 914) pp 457–471
M. Fernandez, AC-Complement Problems: Validity and Negation Elimination Proceedings of 5th RTA, 1993, (Springer LNCS vol. 690) pp. 358–373
D. Lugiez and J.-L. Moysset. Complement problems and tree automata in AC-like theories Proceedings of the Symposium on Theoretical Aspects of Computer Science 1993, (Springer LNCS vol. 665) pp. 515–524
M. Machtey, P. Young, An Introduction to the General Theory of Algorithms, Elsevier 1978
R. Treinen, A New Method for Undecidability Proofs of First Order Theories in Proceedings of the Tenth Conference on Foundations of Software Technology and Theoretical Computer Science, (Springer LNCS 472) volume 472, 1990
R. Treinen, A new method for undecidability proofs of first order theories Journal of Symbolic Computation 14(5) November 1992 pp 437–458
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Marcinkowski, J. (1999). Undecidability of the \( \exists ^ * \forall ^ * \) Part of the Theory of Ground Term Algebra Modulo an AC Symbol. In: Narendran, P., Rusinowitch, M. (eds) Rewriting Techniques and Applications. RTA 1999. Lecture Notes in Computer Science, vol 1631. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48685-2_8
Download citation
DOI: https://doi.org/10.1007/3-540-48685-2_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66201-3
Online ISBN: 978-3-540-48685-5
eBook Packages: Springer Book Archive