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.)
Best Answer
State of the art — yes, so far as I know all algorithms more or less take the same shape as Huet's (I follow theory of logic programming, although my expertise is tangential) provided you need full higher-order matching: subproblems such as higher-order matching (unification where one term is closed), and Dale Miller's pattern calculus, are decidable.
Note that Huet's algorithm is the best in the following sense — it is like a semi-decision algorithm, in that it will find the unifiers if they exist, but it is not guaranteed to terminate if they do not. Since we know that higher-order unification (indeed, second-order unification) is undecidable, you can't do better than that.
Explanations: The first four chapters of Conal Elliott's PhD thesis, Extensions and Applications of Higher-Order Unification should fit the bill. That part weighs almost 80 pages, with some dense type theory, but its well motivated, and is the most readable account I've seen.
Examples: Huet's algorithm will come up with the goods for this example: [X(o), Y(succ(0))]; which of necessity will perplex a first-order unification algorithm.