Modular higher-order equational preunification

Abstract:

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.

FTP: ftp.uni-bremen.de:/pub/Uni-Bremen/Institutes/ZKW/INFORM/qian/heu.ps.gz

For a hard copy send a message to Zhenyu Qian.