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

Feuille d'exercices 10

Unification et résolution au premier ordre

Calculer des unificateurs les plus généraux, réfuter avec des variables, et suivre ce que fait Prolog. Chapitre 10.

Corrigé
  1. $\{x := b,\; y := a\}$.
  2. Décomposer : $x = f(y)$, $f(x) = z$. Éliminer $x$ : $z = f(f(y))$. upg : $\{x := f(y),\; z := f(f(y))\}$.
  3. Échec par le test d'occurrence : on arrive à $y = f(f(y))$ (voir le chapitre 10).
  4. Échec par conflit : $a = b$, deux constantes différentes.
  5. $\{x := g(g(a)),\; y := g(a),\; z := a\}$.
  6. $x = f(y)$ et $x = f(a)$. Éliminer $x$ : $f(y) = f(a)$, puis $y = a$. upg : $\{x := f(a),\; y := a\}$.
Corrigé
  1. Clauses $\lnot \mathit{Homme}(x) \lor \mathit{Mortel}(x)$, $\mathit{Homme}(s)$, $\lnot \mathit{Mortel}(s)$. Résolution des deux premières avec $\{x := s\}$ : $\mathit{Mortel}(s)$ ; avec la troisième : $\square$.
  2. Clauses : (1) $\lnot C(x) \lor G(x)$, (2) $\lnot C(y) \lor \mathit{Car}(y)$, (3) $C(a)$, (4) $\lnot \mathit{Car}(z) \lor \lnot G(z)$. (1) et (3), $\{x := a\}$ : (5) $G(a)$. (2) et (3), $\{y := a\}$ : (6) $\mathit{Car}(a)$. (4) et (6), $\{z := a\}$ : (7) $\lnot G(a)$. (5) et (7) : $\square$.
  3. Prédicats $E$, $T$, $R$, $H$ (étudiant, travaille, réussit, content), constante $m$. Clauses : (1) $\lnot E(x) \lor \lnot T(x) \lor R(x)$, (2) $\lnot E(y) \lor \lnot R(y) \lor H(y)$, (3) $E(m)$, (4) $T(m)$, (5) $\lnot H(m)$. (2) et (5), $\{y := m\}$ : (6) $\lnot E(m) \lor \lnot R(m)$ ; avec (3) : (7) $\lnot R(m)$. (1) et (7), $\{x := m\}$ : (8) $\lnot E(m) \lor \lnot T(m)$ ; avec (3) : (9) $\lnot T(m)$ ; avec (4) : $\square$.
Corrigé
  1. $\mathit{parent}(\mathit{tom}, \mathit{bob})$ ; $\mathit{parent}(\mathit{bob}, \mathit{ann})$ ; $\lnot \mathit{parent}(X, Y) \lor \lnot \mathit{parent}(Y, Z) \lor \mathit{grandparent}(X, Z)$.
  2. But $\lnot \mathit{grandparent}(\mathit{tom}, W)$ avec la troisième clause, upg $\{X := \mathit{tom},\; Z := W\}$ : $\lnot \mathit{parent}(\mathit{tom}, Y) \lor \lnot \mathit{parent}(Y, W)$. Avec $\mathit{parent}(\mathit{tom}, \mathit{bob})$, $\{Y := \mathit{bob}\}$ : $\lnot \mathit{parent}(\mathit{bob}, W)$. Avec $\mathit{parent}(\mathit{bob}, \mathit{ann})$, $\{W := \mathit{ann}\}$ : $\square$. Prolog répond W = ann : la valeur que l'unification a donnée à $W$ en chemin.
Corrigé
  1. On poserait $x := f(x)$, et le terme obtenu serait infini : $f(f(f(\ldots)))$. Aucun terme fini ne convient : l'unification doit échouer.
  2. Elles ne sont pas contradictoires : sur $\mathbb{N}$ avec $P$ l'égalité et $f$ « plus un », $\forall x\, P(x, x)$ est vraie, et $\forall y\, \lnot P(y, f(y))$ aussi ($y \neq y + 1$). Pourtant, sans test d'occurrence, on unifierait $P(x, x)$ et $P(y, f(y))$ en posant $x := y$ puis $y := f(y)$, et l'on dériverait $\square$ : une « preuve » d'une contradiction qui n'existe pas. C'est le prix de la vitesse de Prolog.