Higher-order unification revisited: Complete sets of transformations (Q1823936)

Some approach to higher-order unification is presented. The approach is based on the method of transformation of terms and extends the approach developed by Martelli and Montanari in the context of first-order unification. The method of transformations for solving unification problems is much like the well-known Gaussian method used for solving systems of linear equations. Gaussian elimination and first-order unification are somewhat similar. But in the higher-order case the analogy breaks down. The most important differences to the first-order case have to do with the imitation rule and the generalization of the notion of a partial binding to higher-order substitutions.