Higher-Order and Semantic Unification

Abstract. We provide a complete system of transformation rules for semantic unification with respect to theories defined by convergent rewrite systems. We show that this standard unification procedure, with slight modifications, can be used to solve the satisfiability problem in combinatory logic with a convergent set of algebraic axioms R, thus resulting in a complete higher-order unification procedure for R. Furthermore, we use the system of transformation rules to provide a syntactic characterization for R which results in decidability of semantic unification.

• Type: Conference
• Year: 1993
• Where: FSTTCS
• Authors: Nachum Dershowitz, Subrata Mitra
• Keywords: FSTTCS 1993, Semantic Unification, Software Engineering, Transformation Rules, Unification Procedure