L'objectif principal de l'unification est de rendre égales ou identiques deux expressions symboliques données. L'unification en logique concerne la recherche de substitutions qui transforment une formule donnée en un théorème ou une tautologie. Les substitutions qui réussissent cette transformation sont appelées unifieurs. Le problème crucial de la théorie de l'unification est de trouver des unifieurs aussi généraux que possible, c'est-à-dire des unifieurs dont tous les autres sont des cas particuliers. Il y a 4 types de formules - nullaires, infinitaires, finitaires et unitaires - selon qu'elles possèdent ou non un ensemble minimal complet d'unifieurs et selon la cardinalité de cet ensemble lorsqu'il existe. Le sujet de cet exposé est d'étudier le problème de l'unification, sa complexité et son type dans certaines des logiques de l'intelligence artificielle.