Abstract
A clear distinction is made between the (elementary) unification problem where there is only one pair of terms to be unified, and the problem where many such pairs have to be simultaneously unified — it is shown that there exists a finite, depth-reducing, and confluent term-rewriting system R such that the (single) E-unification problem mod R is decidable, while the simultaneous E-unification problem is undecidable. It is also shown that E-unification is undecidable for variable-permuting theories, thus settling an open problem. The corresponding E-matching problem is shown to be PSPACE-complete.
This work was supported by the Natural Sciences and Engineering Research Council of Canada. It was done while this author was visiting the Dept. of Computer Science, University of Calgary, Alberta, Canada T2N 1N4.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Benanav, D., D. Kapur, and P. Narendran, “Complexity of Matching Problems,” In: Proceedings of RTA-85, Dijon, France. A revised version appears in Journal of Symbolic Computation 3 (1987) 203–216.
Book, R.V., “Confluent and other types of Thue systems,” Journal of the ACM 29 (1982), 171–182.
Book, R.V., M. Jantzen, B. Monien, C. Ó'Dúnlaing, and C. Wrathall, “On the Complexity of Word Problems in certain Thue systems,” Mathematical Foundations of Computer Science, LNCS 118 (1981) 216–223.
Bürckert, H.-J., A. Herold, and M. Schmidt-Schauss, “On Equational Theories, Unification, and (Un)Decidability,” J. of Symbolic Computation 8 (1989) 3–49.
Fages, F., “Associative-Communtative Unification,” In: Proceedings of 7th Conference on Automated Deduction (CADE-84), Napa Valley, California.
Fortenbacher, A., “An Algebraic Approach to Unification under Associativity and Commutativity,” In: Proceedings of RTA-85, Dijon, France.
Hopcroft, J.E., and J.D. Ullman, Introduction to Automata Theory, Languages and Computation, Addison-Wesley, 1979.
Huet, G., and D. Oppen, “Equations and Rewrite Rules: a survey,” in Formal Languages: Perspectives and Open Problems (R. Book, ed.), Academic Press, New York, 1980.
Otto, F., “Some Undecidability Results for Non-Monadic Church-Rosser Thue systems,” Theoretical Computer Science 33 (1984) 261–278.
Otto, F., “On Two Problems Related to Cancellativity,” Semigroup Forum 33 (1986), 331–356.
Schmidt-Schauss, M.J., “Two Problems in Unification Theory,” Bulletin of the EATCS 34 (Feb '88) p. 273.
Siekmann, J.H., “Universal Unification,” In: Proceedings of CADE-7, Napa Valley, CA, LNCS 170 (1984) 1–42.
Siekmann, J.H., “Unification Theory,” Journal of Symbolic Computation 7 (1989) 207–274.
Stickel, M.E., “A Unification Algorithm for Associative-Commutative Functions,” Journal of the ACM 28, 423–434.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Narendran, P., Otto, F. (1990). Some results on equational unification. In: Stickel, M.E. (eds) 10th International Conference on Automated Deduction. CADE 1990. Lecture Notes in Computer Science, vol 449. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52885-7_94
Download citation
DOI: https://doi.org/10.1007/3-540-52885-7_94
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52885-2
Online ISBN: 978-3-540-47171-4
eBook Packages: Springer Book Archive