MODULAR HIGHER-ORDER EQUATIONAL PREUNIFICATION

Preunification of simply typed X-terms with respect to the equivalence relation induced by alpha-, beta- eta-conversion and an arbitrary fir st-order equational theory is useful in higher-order proof and logic p rogramming systems. In this paper we present a procedure for such preu nification, which is based on three transformations and parameterized by a first-order equational unification procedure that admits free fun ction symbols. The procedure is proved to be sound and complete, provi ded that the parameterizing procedure is. (C) 1996 Academic Press Limi ted.