E-Unification
Wayne Snyder · Birkhäuser Boston eBooks · 1991
In Section §3.3 we defined the standard unification of terms, most general unifiers, and showed how the abstract non-deterministic method of transformations on systems of equations provides a procedure for unification which either fails or terminates with an explicit representation of the mgu of the original system. The notion of standard unification is based on making two (first-order) terms syntactically identical, but in fact, we could generalize this to any relation P on terms, defining “ P -unification” to be the problem of determining for two terms u and v if there exists some substitution θ such that ( θ ( u ), θ ( v ))∊ P . In this section we present the basic notions of E -unification, where this relation P is represented by a finite set of equations E . The two following chapters will present a general procedure for E -unification via the method of transformations; later in this monograph, in Chapter §7, we present a generalization of unification to higher-order terms, and develop a non-deterministic procedure in the same fashion. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.