| In this thesis a new approach to solving the E-unification problem is laid out and explored. This approach is goal-directed, because it searches for a solution for an equation by analyzing the structure of this equation, as opposed to procedures based on a completion of an equational theory. It is top-down, since it analyzes the goal and applies inference rules to the goal only with respect to the top symbols in the terms in the goal equation. Such a goal-directed, top-down procedure is presented and proved to be complete for a general E-unification problem for any equational theory. This is a semi-decision procedure.; Next we examine different ways to put syntactic restrictions on an equational theory for which we want to solve an E-unification problem, so that this semi-decision procedure becomes a decision procedure (it always terminates).; Hence we are able to prove complexity results for E-unification in classes of equational theories.; Finally we prove completeness of the goal-directed, top-down procedure with Variable Elimination eagerly applied. Solving this problem opens new ways to find still more classes of equational theories for which some form of E-unification is decidable and the complexity may be found. |
