Title
A combinatory logic approach to higher-order E-unification
Abstract
Let E be a first-order equational theory. A translation of higher-order E -unification problems into a combinatory logic framework is presented and justified. The case in which E admits presentation as a convergent term rewriting system is treated in detail: in this situation, a modification of ordinary narrowing is shown to be a complete method for enumerating higher-order E -unifiers. In fact, we treat a more general problem, in which the types of terms contain type variables.
Year
DOI
Venue
1995
10.1016/0304-3975(94)00210-A
Theor. Comput. Sci.
Keywords
DocType
Volume
combinatory logic approach
Journal
139
Issue
ISSN
Citations 
1-2
Theoretical Computer Science
1
PageRank 
References 
Authors
0.43
7
2
Name
Order
Citations
PageRank
Daniel J. Dougherty141332.13
Patricia Johann210.43