E-Unification via Transformations
Wayne Snyder · Birkhäuser Boston eBooks · 1991
We now show how to extend the set of transformations ST given in Section §3.3 to perform E -unification of a system under some arbitrary E , and develop the non-deterministic completeness of the method using a new formalism for ‘proofs’ that two terms are E -unifiable, known as equational proof trees . The new set of transformations is fully general in that it is capable of enumerating a CSU E ( S ) for any system S and set of equations E , and we intend this chapter to provide a paradigm for the abstract study of complete methods for general E -unification. The set of E -unifiers found by this method is highly redundant, however, and in the next chapter, we show how to restrict this method to avoid rewriting at variable occurrences while still retaining the ability to enumerate a CSU E ( S ). 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.