A combinatory logic approach to higher-order $E$-unification. Dougherty, D. J.\ & Johann, P. Theoretical Computer Science, 139(1--2):207--242, 1995.
A combinatory logic approach to higher-order $E$-unification [pdf]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.

Downloads: 0