Abstract
For finite convergent term-rewriting systems the equational unification problem is shown to be recursively independent of the equational matching problem, the word matching problem, and the (simultaneous) 2nd-order equational matching problem. We also present some new decidability results for simultaneous equational unification and 2nd-order equational matching.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Avenhaus, J., and K. Madlener, “Term Rewriting and Equational Reasoning,” in: R.B. Banerji (ed.), Formal Techniques in Artificial Intelligence, North-Holland, Amsterdam, 1990, pp. 1–43.
Baader, F., and J. Siekmann, “Unification Theory,” in: D.M. Gabbay, C.J. Hogger and J.A. Robinson (eds.), Handbook of Logic in Artificial Intelligence and Logic Programming, Oxford University Press, Oxford, UK, 1993.
Book, R.V., and F. Otto, String-Rewriting Systems, Springer: New York, 1993.
Bürckert, H.-J., “Matching-a special case of unification?” Journal of Symbolic Computation 8 (1989) 523–536.
Dershowitz, N., and J.P. Jouannaud, “Rewrite Systems,” in: J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, Vol. B: Formal Models and Semantics, Elsevier, Amsterdam, 1990, pp. 243–320.
Farmer, W.M., “A unification algorithm for second-order monadic terms,” Annals of Pure and Applied Logic 39 (1988) 131–174.
Goldfarb, W.D., “The undecidability of the second-order unification problem,” Theoretical Computer Science 13 (1981) 225–230.
Makanin, G.S., “The problem of solvability of equations in a free semigroup,” Math. USSR Sbornik 32 (1977) 129–198.
Narendran, P., and F. Otto, “Some results on equational unification,” in: M. Stickel (ed.), 10th Int. Conf. on Automated Deduction, Proceedings, Lecture Notes in Artificial Intelligence 449, Springer, Berlin, 1990, pp. 276–291.
Otto, F., “On two problems related to cancellativity,” Semigroup Forum 33 (1986) 331–356.
Otto, F., “Solvability of word equations modulo finite special and confluent string-rewriting systems is undecidable in general,” Information Processing Letters, to appear.
Otto, F., The 2 nd-tOrder E-Unification Problem for Finite Monadic String-Rewriting Systems, in preparation.
Pécuchet, J.-P., Equations avec Constantes et Algorithme de Makanin, Thèse 3e Cycle, Université de Rouen, France, 1981.
Schulz, K.U., “Makanin's Algorithm for Word Equations-Two Improvements and a Generalization,” in: K.U. Schulz (ed.), Word Equations and Related Topics, Proceedings, Lecture Notes in Computer Science 572, Springer, Berlin, 1990, pp. 85–150.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Otto, F., Narendran, P., Dougherty, D.J. (1995). Some independence results for equational unification. In: Hsiang, J. (eds) Rewriting Techniques and Applications. RTA 1995. Lecture Notes in Computer Science, vol 914. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59200-8_70
Download citation
DOI: https://doi.org/10.1007/3-540-59200-8_70
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59200-6
Online ISBN: 978-3-540-49223-8
eBook Packages: Springer Book Archive