Unification is a tool for solving a collection of equations over a free algebra.

A substitution is an equation with just a variable on the left-hand side. A collection of substitutions is proper if no variable that occurs on the left-hand side of any of those substitutions also occurs on the right-hand side of any of the substitutions.

When an equation has a solution, unification converts it into a group of proper substitutions. Then the substitutions can be used to eliminate the variables on left-hand sides of substitutions.

When an equation is not solvable, unification reports that it is not solvable.