We present a semi-decision algorithm for the unifiability of two set-theoretic formulas modulo -reduction. The algorithm is based on the approach developed by G. Huet for type theory, but requires additional measures because formulas in set theory are not all normalizable. We present the algorithm in an Ada-like pseudocode, and then prove two theorems that show the completeness and correctness of the procedure. We conclude by showing that -unification is not a complete quantifier substitution method for set theory-unlile first-order unification and first-order logic. In this respect set theory is similar to type theory (higher-order logic).