Calcul des prédicats : les unifications

Sommaire du document

Unification

Si nous avons un ensemble d'équations P de la forme  { t₁ / s₁, ..., t_n / s_n }  où tout t et tout s sont des termes, nous pouvons parler de problème d'unification; il est peut-être possible de trouver une substitution qui joue le rôle d'unificateur.

Nous pouvons unifier les deux termes t₁, t₂ ssi  ∃ une substitution σ : t₁σ = t₂σ. Le signe « = » correspond ici à une égalité syntaxique.
La substitution σ porte le nom d'unificateur de t₁ et t₂.

Nous parlons de l'ensemble des unificateurs (nous noterons U(P) l'ensemble des unificateurs de P), car pouvons avoir plus d'un unificateur pour une même substitution. Nous dirons donc que P est unifiable si U(P) ≠ ∅.

Particularité

Nous dirons d'une substitution α qu'elle est plus particulière qu'une autre substitution β s'il existe une substitution σ telle que α = βσ. Nous noterons la particularité comme ceci : α ⊴ β.

MGU

Un mgu de deux termes est un unificateur α tel que pour tout autre unificateur β de ces deux termes, β est plus particulier que α

Nous pouvons déterminer le mgu de deux termes gràce à l'algorithme d'unification de Herbrand.

Notes

1. ↑ ssi : si et seulement si
   
   
2. ↑^a,b most general unifier : correspond à « unificateur le plus général” en français
   
   
3. ↑^a,b mgu : “most general unifier” (en français, « unificateur le plus général »)
   
   

Références

1. IHDCB337 - Technique d'intelligence artificielle : JM Jacquet, Programmation déclarative (2009)
2. IHDCB337 - Technique d'intelligence artificielle : H Toussaint, Tp (2009)
3. Logique pour l'informatique : Serenella Cerrito, Introduction à la déduction automatique (Octobre 2008)

Ces références et liens indiquent des documents consultés lors de la rédaction de cette page, ou qui peuvent apporter un complément d'information, mais les auteurs de ces sources ne peuvent être tenus responsables du contenu de cette page.
L'auteur de ce site est seul responsable de la manière dont sont présentés ici les différents concepts, et des libertés qui sont prises avec les ouvrages de référence. N'oubliez pas que vous devez croiser les informations de sources multiples afin de diminuer les risques d'erreurs.

Structure du document