Algorithme d'unification
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.
| 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 |
Utilisateur : Timothée
Références :
Introduction à la logique - René David, Karim Nour, Christophe Raffalli (DNR)