Développement #192

Titre : Algorithme d'unification

Contenu : 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.

Créé le : 23/07/2026 12:42

Mis à jour : 23/07/2026 12:42

✏️ Modifier
Qualité Numéro Titre
5 917 Logique du premier ordre : syntaxe et sémantique.2016
5 919 Unification : algorithmes et applications.2017
5 927 Exemples de preuve d’algorithme : correction, terminaison.2021