Version sans JavaScript, en lecture seule : les ateliers, les quiz et l’exécution du code n’y sont pas. Version complète · Catalogue · Se connecter
Support de cours · chapitre 10
Unification et résolution au premier ordre
Trouver la substitution la plus générale qui rend deux termes égaux, s'en servir pour résoudre des clauses avec variables, et ce que la machine peut, ou ne peut pas, décider.
Le problème
Les clauses $\lnot \mathit{Homme}(x) \lor \mathit{Mortel}(x)$ et $\mathit{Homme}(\mathit{socrate})$ devraient donner $\mathit{Mortel}(\mathit{socrate})$. Mais la règle du chapitre 5 exige un littéral et son exact opposé, et $\mathit{Homme}(x)$ n'est pas $\mathit{Homme}(\mathit{socrate})$. Comme la variable $x$ de la première clause vaut pour tout objet (elle est implicitement quantifiée par $\forall$), on peut la spécialiser : en remplaçant $x$ par $\mathit{socrate}$, les deux littéraux deviennent opposés. Trouver ce remplacement s'appelle l'unification.
Substitutions et unificateurs
Substitution
Une substitution $\sigma = \{x_1 := t_1, \ldots, x_n := t_n\}$ remplace simultanément chaque variable $x_i$ par le terme $t_i$. On note $t\sigma$ le résultat sur un terme $t$ (et $L\sigma$ sur un littéral).
Exemple : $f(x, g(y))\{x := a,\; y := h(x)\} = f(a, g(h(x)))$. Le $x$ introduit par $h(x)$ n'est pas remplacé à son tour : le remplacement est simultané.
Unificateur
Un unificateur de deux termes (ou de deux atomes) $s$ et $t$ est une substitution $\sigma$ telle que $s\sigma = t\sigma$.
$f(x, a)$ et $f(b, y)$ ont pour unificateur $\{x := b, y := a\}$ : les deux deviennent $f(b, a)$.
Deux termes peuvent avoir beaucoup d'unificateurs. $g(x)$ et $g(y)$ sont unifiés par $\{x := y\}$, mais aussi par $\{x := a, y := a\}$, qui en dit plus que nécessaire. On cherche l'unificateur le plus général (en abrégé, upg) : celui qui ne fixe que ce qui est indispensable, et dont tous les autres sont des cas particuliers. Ici, $\{x := y\}$.
L'algorithme d'unification
On part de l'équation $s = t$ et on applique ces règles tant qu'on peut, à un ensemble d'équations (algorithme de Robinson, 1965, sous la forme de Martelli et Montanari) :
| Règle | Si l'on a | On fait |
|---|---|---|
| Décomposer | $f(s_1, \ldots, s_n) = f(t_1, \ldots, t_n)$ | remplacer par $s_1 = t_1, \ldots, s_n = t_n$ |
| Conflit | $f(\ldots) = g(\ldots)$, avec $f \neq g$ (ou des constantes différentes) | échec |
| Effacer | $t = t$ | supprimer l'équation |
| Orienter | $t = x$, où $t$ n'est pas une variable | la retourner : $x = t$ |
| Test d'occurrence | $x = t$, où $x$ apparaît dans $t$ (et $t \neq x$) | échec |
| Éliminer | $x = t$, où $x$ n'apparaît pas dans $t$ | remplacer $x$ par $t$ dans toutes les autres équations |
À la fin, s'il n'y a pas eu d'échec, il reste des équations $x_1 = t_1, \ldots, x_n = t_n$ : c'est l'upg.
La résolution au premier ordre
La règle
Soit deux clauses sans variable commune (on renomme au besoin), $C \lor P(s_1, \ldots, s_n)$ et $D \lor \lnot P(t_1, \ldots, t_n)$. Si $P(s_1, \ldots, s_n)$ et $P(t_1, \ldots, t_n)$ ont un upg $\sigma$, la résolvante est :
On applique la substitution à tout ce qui reste, pas seulement aux littéraux résolus.
La résolution complète utilise aussi la factorisation : si deux littéraux d'une même clause sont unifiables, on peut les fusionner, en appliquant leur upg à la clause. On en a rarement besoin dans les exercices.
Théorème (Robinson, 1965). Un ensemble de clauses du premier ordre est insatisfiable si et seulement si on peut en dériver $\square$ par résolution et factorisation. (Admis.)
La méthode complète
Pour montrer $\Sigma \vDash A$ :
- prendre $\Sigma \cup \{\lnot A\}$ ;
- mettre chaque formule en forme prénexe, skolémiser, passer en clauses (chapitre 9) ;
- renommer les variables pour qu'aucune clause n'en partage avec une autre ;
- dériver $\square$ par résolution, en unifiant à chaque étape.
Ce que la machine peut décider
Au calcul propositionnel, la validité est décidable : une table de vérité répond toujours, même lentement. Au premier ordre, ce n'est plus le cas.
Théorème (Church et Turing, 1936). Il n'existe aucun algorithme qui, pour toute formule du premier ordre, décide si elle est valide.
La résolution donne malgré tout une semi-décision : si la formule est valide, la recherche finira par trouver $\square$ ; si elle ne l'est pas, la recherche peut ne jamais s'arrêter. C'est le mieux qu'on puisse faire.
Prolog exploite cette situation. Un programme Prolog est un ensemble de clauses de Horn du premier ordre, une question est un but à réfuter, et l'interpréteur fait de la résolution avec unification, dans un ordre fixé. Par défaut, il omet le test d'occurrence, pour aller plus vite : il accepte alors d'unifier X et f(X), ce que l'algorithme de ce chapitre refuse.
Ce qu'on a fait
Le cours a suivi un seul fil : savoir si une affirmation découle d'autres. On l'a posé sur les propositions, en lisant les formules (chapitre 1) et en leur donnant un sens (chapitre 2). On a appris à les transformer (chapitre 3), à les faire résoudre (chapitre 4), à les réfuter (chapitre 5) et à les prouver (chapitre 6). Puis on a tout repris avec des objets et des quantificateurs (chapitres 7 à 10), jusqu'à la limite de ce qu'une machine peut décider.