Unification algorithms form the core of almost all automated deduction systems, and generalizations of the basic paradigms to first-order logic with equality and to higher-order logic have motivated the design of more general forms of unification. This report proposes to continue the PI's work in developing a theory of general unification using the method of transformation on systems of terms invented by Herbrand. Also under investigation is the development of the first known algorithm for general E-unification and new techniques for implementing higher-order unification. In addition, an extension of Andrew's method of matings to account for equality, which involves a new form of unification called rigid E-unification will be studied.
