Unification is a generalization of pattern matching where both the “pattern” and the “datum” may contain variables.
A unifier takes two patterns, and determines whether it is possible to assign values to the variables that make the two patterns equal. For example, unifying (?x a ?y) and (?y ?z a) will get the result where ?x ?y ?z are all bounded to a. On the other hand, unifying (?x ?y a) and (?x b ?y) will fail.1