Modular higher-order equational preunification


Preunification of simply typed lambda terms with respect to the equivalence relation induced by alpha-, beta- and eta-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.

The paper is here.

Zhenyu Qian.