In the area of theorem proving, one often faces the problem of constructing a unification algorithm for the theory under consideration. For a class of theories, it is possible to automatically construct a unification algorithm from the so-called “resolvent presentation” of the theory. The authors present an algorithm that computes the resolvent via a completion technique if it terminates. A proof of its correctness and completeness is provided.