Unification is essentially a process of substitution. I have seen it called "two-way matching".

In Prolog, in other logic programming languages and in languages directly based on rewriting logic (Maude, Elan, etc...) is the mechanism by which free (logical) variables are bind to terms/values. In Concurrent Prolog these variables are interpreted as communication channels.

IMO, the better way to understand it is with some examples from mathematics (unification was/is a base key mechanism, for example, in the context of automated theorem provers research, a sub-field of AI; another use in in type inference algorithms). The examples that follow are taken from the context of computer algebra systems (CAS):

First example:

given a set Q and two binary operations * and + on it, then * is left-distributive over + if:

X * (Y + Z)   =   (X * Y) + (X * Z)   |1|

this is a rewrite rule (a set of rewrite rules is a rewriting system).

If we want to apply this rewrite rule to a specific case, say:

a * (1 + b)   |2|

we unify (via a unification algorithm) this term, |2|, with the left-hand side (lhs) of |1| and we have this (trivial on purpose) substitution (the most general unifier, mgu):

{X/a, Y/1, Z/b}   |3|

Now, applying |3| to the right-hand side (rhs) of |1|, we have, finally:

(a * 1) + (a * b)

This was simple and to appreciate what unification can do I will show a little more complex example.

Second example:

Given this rewrite rule:

log(X,Y) + log(X,Z)   =>   log(X,Y*Z)   |4|

we apply it to this equation:

log(e,(x+1)) + log(e,(x-1)) = k   |5|

(lhs of |5| unify to lhs of |4|), so we have this mgu:

{X/e, Y/(x+1), Z/(x-1)}   |6|

Note that X and x are two different variables. Here we have two variables, X and Y, which match two compound terms, (x+1) and (x-1), not simple values or variables.

We apply this mgu, |6|, to rhs of |4| then and we put back this in |5|; so we have:

log(e,(x+1)*(x-1)) = k   |7|

and so on.

(Hoping I did not any mistake or this may confuse neophytes even more.)

Unification is a key mechanism in type inference. Practically speaking, unification in this context will greatly reduce wear on your fingers.

Prolog, for instance, uses unification to find values for variables that satisfy the rules - see this explanation for an example. I expect it s a typical technique in logical programming languages in general, though I don t have experience with any others.

Unification is like pattern-matching, where you rub together two structures, where variables in one are allowed to match values in the other.

The simplest form of unification happens whenever you call a function in a normal language. The caller has arguments, and the callee has parameters. The parameters are "bound to" the arguments, and that produces an instantiation of the function.

Another simple form of unification is when you use a regular expression for matching, for example at a command prompt you might say dir x*y*.z* which will match some but not all file names.

Artificial Intelligence likes to make use of inference engines, to try to simulate reasoning from a corpus of knowledge, usually in the form of statements in a logic. To pick a stupid example, you might "know" that "all men are mortal", as in forall(x)(man(x) implies mortal(x)). Then if you ask a question "is Sam mortal" as mortal(Sam)?, you could unify that with the rule to get a new question "is Sam a man" man(Sam)?

Hope that helps.