The monograph presents an approach to general E-unification and higher-order unification based on applying the non-deterministic transformations for systems of equations as originated from Herbrand and developed, in the case of standard first-order unification, by Martelli and Montanari. The mathematical formalism which is used permits an effective separation of the logical instruments from the specification of the procedural information and provides rigorous means for analysing the properties of these more complex types of unification problems. In both cases, the basic set of transformation rules for standard unification is extended by capturing the essential scheme which makes terms identical in these two generalizations of unification, i.e. the least congruence induced by the set of equations for E- unification, and modulo the conversion rules of the typed lambda-calculus for the higher-order unification.
by Wayne Snyder
Unification Theory
All articles published by Studies in Informatics and Control (SIC) are published in accordance with the terms and conditions of the Creative Commons Attribution License (CC BY-NC-SA 4.0).