 A most general unifier (mgu) produces the most general instance shared by two unifiable expressions. In the previous example, the substitution {x ← b, y ← b, z ← f(a,b)} is a unifier but not an mgu; however, {x ← b, z ← f(a,y)} is an mgu. Note that unification attempts to “match” two expressions and this fundamental process has become a central component of most automated deduction programs, resolution-based and otherwise. Theory-unification is an extension of the unification mechanism that includes built-in inference capabilities. For example, the clauses R(g(a,b),x) and R(g(b,a),d) do not unify but they AC-unify, where AC-unification is unification with built-in associative and commutative rules such as g(a,b) = g(b,a). Shifting inference capabilities into the unification mechanism adds power but at a price: The existence of an mgu for two unifiable expressions may not be unique (there could actually be infinitely many), and the unification process becomes undecidable in general. 