Développement : Algorithme d'unification

Détails/Enoncé :

On montre que si l'algorithme d'unification termine avec $E_n = \emptyset$, alors la substitution $\sigma$ est l'unification la plus générale du système d'équations donné. S'il échoue alors le système d'équations n'a pas d'unification.

Recasages pour l'année 2024 :

  • Pas de recasages pour cette année.

Références utilisées dans les versions de ce développement :

Introduction à la logique, René David, Karim Nour, Christophe Raffalli (DNR) (utilisée dans 16 versions au total)