Modular Higher-Order EquationalPreunification

Preunification of simply typed λ-terms with respect to the equivalence relation induced by α-, β- and η-conversion and an arbitrary first-order equational theory is useful in higher-order proof and logic programming systems. In this paper we present a procedure for such preunification, which is based on three transformations and parameterized by a first-order equational unification procedure that admits free function symbols. The procedure is proved to be sound and complete, provided that the parameterizing procedure is.