#### Modular Higher-Order E-Unification

#### Tobias Nipkow, Zhenyu Qian

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 lambda-terms w.r.t. the union of alpha, beta and
eta 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.
SpringerLink

BibTeX:

@inproceedings{Nipkow-Qian-RTA-91,
author="Tobias Nipkow and Zhenyu Qian",
title="Modular Higher-Order {$E$}-Unification",
booktitle="Proc.\ 4th Int.\ Conf.\ Rewriting Techniques and Applications",
editor="R.V. Book",
year=1991,publisher=Springer,series=LNCS,volume=488,pages="200--214"}