Unification

Le processus consistant à trouver des substitutions pour les variables qui rendent deux expressions syntaxiques (termes) identiques selon l'algèbre des termes d'une logique ; il produit une substitution associant variables à termes lorsqu'une solution existe.