Regular paperA combinatory logic approach to higher-order E-unification☆
Review articleOpen access

AbstractLet 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.

Request full text

References (0)

Cited By (0)

No reference data.
No citation data.
Join Copernicus Academic and get access to over 12 million papers authored by 7+ million academics.
Join for free!