Abstract
The combination of higher-order and first-order unification algorithms is studied. We present algorithms to compute a complete set of unifiers of two simply typed λ-terms w.r.t. the union of α, β and η conversion and a first-order equational theory E. The algorithms are extensions of Huet’s work and assume that a complete unification algorithm for E is given. Our completeness proofs require E to be at least regular.
Cite
CITATION STYLE
Nipkow, T., & Qian, Z. (1991). Modular higher-order E-unification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 488 LNCS, pp. 200–214). Springer Verlag. https://doi.org/10.1007/3-540-53904-2_97
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
