Paper Info
Title
Equational unification, word unification, and 2nd-order equational unification
Abstract
For finite convergent term-rewriting systems it is shown that the equational unification problem is recursively independent of the equational matching problem , the word matching problem , and the 2nd- order equational matching problem . Apart from the latter these results are derived by considering term-rewriting systems on signatures that contain unary function symbols only (i.e., string-rewriting systems). Also for this special case 2nd-order equational matching is shown to be reducible to 1st-order equational matching. In addition, we present some new decidability results for simultaneous equational matching and unification . Finally, we compare the word unification problem to the 2nd- order equational unification problem .
Year
DOI
Venue
1998
10.1016/S0304-3975(97)00130-8
Theor. Comput. Sci.
Keywords
DocType
Volume
word unification,String-rewriting systems,Term-rewriting systems,2nd-order equational matching and unification,equational unification,Equational matching and unification
Journal
198
Issue
ISSN
Citations 
1-2
Theoretical Computer Science
0
PageRank 
References 
Authors
0.34
9
3
Name
Order
Citations
PageRank
Friedrich Otto117118.72
Paliath Narendran21100114.99
Daniel J. Dougherty341332.13