unification

concept processus algorithmique qui, étant donnés deux termes, trouve une substitution qui appliquée aux deux termes les rend identiques