A combinatory logic approach to higher-order $E$-unification. Dougherty, D. J.\ and Johann, P. Theoretical Computer Science, 139(1--2):207--242, 1995.
Paper abstract bibtex Let E be a first-order equational theory. A translation of typed higher-order E-unification problems into a typed 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.
@article{ a_tcs95,
author = {Daniel J.\ Dougherty and Patricia Johann},
title = {A combinatory logic approach to higher-order
{$E$}-unification},
journal = {Theoretical Computer Science},
volume = {139},
number = {1--2},
pages = {207--242},
day = {06},
year = {1995},
issn = {0304-3975},
pubcountry = {Netherlands},
abstract = {Let E be a first-order equational theory. A
translation of typed higher-order E-unification
problems into a typed 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. },
url = {tcs95.pdf}
}