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.



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",