Conclusion

In this monograph we studied general E-unification and higher-order unification using the method of non-deterministic transformations on systems of equations originated by Herbrand and developed in the case of standard first-order unification by Martelli and Montanari. This formalism provides an abstract and mathematically elegant means of analysing the properties of these more complex types of unification problems by providing a clean separation of the logical issues from the specification of procedural information.In each case, we extended the basic set of transformations ST for standard unification by analysing the precise manner in which terms are defined to be ’the same’ in these two generalizations of unification, i.e., modulo the least congruence induced by the set of equations for E-unification,and modulo the conversion rules of the typed lambda calculus for higher-order unification.