What is the difference between unification and anti-unification? I understand that in Unification we try to find a general solution to an equation between two terms, but what is anti-unification, and how is it different?
The following category theory inspired analysis (adapted from Plotkin's A Note on Inductive Generalization) explains a sense in which unification and anti-unification are dual concepts. As notation, let's write
$$t \underset{\sigma}{\Longrightarrow} u$$
for two terms $t$ and $u$ and a substitution $\sigma$ whenever $t\sigma = u$.  The existence of such a subsitution $\sigma$ implies that $t$ is a generalization of $u$, and that $u$ is a specialization of $t$.

Suppose given two terms $t_1,t_2$.  A unifier of $t_1$ and $t_2$ is a term $u$ together with a pair of substitutions $\sigma_1$ and $\sigma_2$ such that
$$
t_1 \underset{\sigma_1}{\Longrightarrow} u \underset{\sigma_2}{\Longleftarrow} t_2
$$
It is a most general unifier if it is a generalization of any other unifier, that is, if for any other unifier
$$
t_1 \underset{\sigma_1'}{\Longrightarrow} u' \underset{\sigma_2'}{\Longleftarrow} t_2
$$
there is some $\sigma'$ such that
$$
u \underset{\sigma'}{\Longrightarrow} u'
$$
In other words, a most general unifier is precisely a coproduct in the category $\mathcal{C}$ whose objects are terms and where there is a morphism $t \to u$ just in case $t \underset{\sigma}{\Longrightarrow} u$ for some $\sigma$.

To define anti-unification we just reverse all the arrows!  Which is to say that...

An anti-unifier of $t_1$ and $t_2$ is a term $u$ together with a pair of substitutions $\sigma_1$ and $\sigma_2$ such that
$$
t_1 \underset{\sigma_1}{\Longleftarrow} u \underset{\sigma_2}{\Longrightarrow} t_2
$$
It is a least general anti-unifier if it is a specialization of any other anti-unifier, that is, if for any other anti-unifier
$$
t_1 \underset{\sigma_1'}{\Longleftarrow} u' \underset{\sigma_2'}{\Longrightarrow} t_2
$$
there is some $\sigma'$ such that
$$
u' \underset{\sigma'}{\Longrightarrow} u
$$
This means that a least general anti-unifier is precisely a product in the category $\mathcal{C}$ defined above.



Update: fixed the accidentally dualized terminology in the original description (thanks Yann Hamdaoui!).