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 matchingprobtem. We also present some new decidability results for simultaneous equational unification and 2nd -order equational matching.
CITATION STYLE
Otto, F., Narendran, P., & Dougherty, D. J. (1995). Some independence results for equational unification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 914, pp. 367–381). Springer Verlag. https://doi.org/10.1007/3-540-59200-8_70
Mendeley helps you to discover research relevant for your work.