@inproceedings{4fddb441437641a6b1983c2ecbbb5233,
title = "Modular higher-order E-unification",
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{\textquoteright}s work and assume that a complete unification algorithm for E is given. Our completeness proofs require E to be at least regular.",
author = "Tobias Nipkow and Zhenyu Qian",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1991.; 4th International Conference on Rewriting Techniques and Applications, RTA-1991 ; Conference date: 10-04-1991 Through 12-04-1991",
year = "1991",
doi = "10.1007/3-540-53904-2_97",
language = "English",
isbn = "9783540539049",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "200--214",
editor = "Book, {Ronald V.}",
booktitle = "Rewriting Techniques and Applications - 4th International Conference, RTA-1991, Proceedings",
}