En informatique et en logique, l'unification est un processus algorithmique qui, étant donnés deux termes, trouve une substitution qui appliquée aux deux termes les rend identiques[1]. Par exemple, et peuvent être rendus identiques par la substitution et , qui donne quand on l'applique à chacun de ces termes le terme . Dit autrement, l'unification est la résolution d'une équation dans l'algèbre des termes (unification syntaxique) ou dans une algèbre quotient par un ensemble d'identités (unification modulo une théorie) ; la solution de l'équation est la substitution qui rend les deux termes identiques et que l'on appelle l'unificateur. L'unification a des applications en inférence de types, programmation logique, en démonstration automatique de théorèmes, en système de réécriture, en traitement du langage naturel[1].
Souvent, on s'intéresse à l'unification syntaxique où il faut que les termes obtenus par application de l'unificateur soient syntaxiquement égaux, comme dans l'exemple ci-dessus. Par exemple, le problème d'unification syntaxique ayant pour données et n'a pas de solution[2]. Le filtrage par motif (ou pattern matching) est une restriction de l'unification où l'unificateur n'est appliquée qu'à un seul des deux termes. Par exemple, et sont rendus égaux par la substitution .
La fin de l'article présente aussi l'unification modulo une théorie, qui est le cas où on dispose de connaissances supplémentaires sur les fonctions (par exemple, est commutatif).