diapos/logique/unif.tex

   1 \frame{
   2  \frametitle{Résolution du premier ordre et unification}
   3  \framesubtitle{Introduction}
   4  \begin{itemize}
   5   \item Partie II du chapitre 7 du cours
   6   \item Méthode syntaxique pour détecter les formules du
   7   premier ordre contradictoires
   8   \item \pause Etapes
   9     \begin{itemize}
  10       \item
  11        \textbf{Réductions} successives de la formule
  12
  13        \begin{enumerate}
  14         \item \pause Mise en forme prénexe
  15         \item \pause Skolémisation : \pause élimination des $\exists$
  16         \item \pause Mise en CNF (\emph{Conjunctive Normal Form})
  17        \end{enumerate}
  18
  19         La formule devient un ensemble de \emph{clauses} du premier
  20         ordre (avec variables)
  21
  22       \item \textbf{Déduction} de nouvelles clauses
  23
  24         Deux règles de déduction : résolution et factorisation
  25             \end{itemize}
  26   \item \pause Théorème : formule initiale contradictoire
  27    si et seulement si la clause vide est déduite
  28  \end{itemize}
  29 }
  30
  31 \frame{
  32  \frametitle{Résolution du premier ordre}
  33  \framesubtitle{Règles de déduction}
  34  \begin{itemize}
  35  \item Résolution
  36
  37   $$
  38   \frac{a \lor \Gamma, \quad \neg b \lor \Delta}{(\Gamma \vee
  39   \Delta) \sigma }
  40    $$
  41
  42
  43   $\sigma$ est l'unificateur le plus général de $a$ et de $b$
  44
  45   \item \pause Factorisation
  46
  47   $$\frac{a \ou b \ou \Gamma}{(b \ou \Gamma) \sigma}$$
  48
  49   $\sigma$ est un unificateur de $a$ et $b$
  50
  51   \item \pause Exemple :
  52   $\{ p(x) \ou p(y) \ou q(z) \} \vdash p(y) \ou q(z)$
  53   car $[x := y]$ est un unificateur de $p(x)$ et $p(y)$
  54  \end{itemize}
  55 }
  56
  57 \begin{frame}
  58 \frametitle{Unification}
  59 \framesubtitle{Exemple et définition}
  60 \begin{itemize}
  61   \item Question : les atomes $R(h(x),y)$ et $R(z,h(a))$, où
  62   $x$ et $y$ sont des variables, peuvent-ils être égaux ?
  63   \item \pause Oui. Ils sont ``unifiables'' avec la substitution
  64    $\sigma = [z:= h(x), y:= h(a)]$ car
  65
  66    $R(h(x),y) \sigma = $ \pause $R(h(x),h(a))$
  67
  68    \pause et
  69
  70    $R(z,h(a)) \sigma = $ \pause $R(h(x),h(a))$
  71   \item \pause Définition : $\sigma$ est un unificateur des termes $s$
  72   et $t$ si $s \sigma = t \sigma$
  73   \item \pause Autrement dit, $\sigma$ est une solution de l'équation
  74    $R(h(x),y) = R(z,h(a))$  dans l'alg\`{e}bre des termes
  75 \end{itemize}
  76 \end{frame}
  77
  78 \begin{frame}
  79 \frametitle{Unification}
  80 \framesubtitle{}
  81 \begin{itemize}
  82   \item $[z:= h(x), y:= h(a)]$ est une solution de l'équation
  83    $R(h(x),y) = R(z,h(a))$
  84   \item \pause Y a t'il plusieurs solutions ?
  85   \item \pause Oui : \pause si $\sigma$ est un unificateur,
  86   alors $\sigma ; \theta$ en est un aussi, pour toute substitution
  87   $\theta$
  88   \item \pause Il y a donc une infinité de solutions !
  89   \item Heureusement, l'équation $t = t'$ admet une solution
  90   minimale unique, génératrice de toutes les solutions
  91   \begin{itemize}
  92       \item  \pause appelée ``unificateur le plus général''
  93       \item  \pause notée $mgu(t,t')$
  94       \item  \pause de support inclus dans $var(t) \cup var(t')$
  95   \end{itemize}
  96   \item \pause Toute autre solution $\alpha$ est moins générale que
  97   $mgu(t,t')$, c'est-à-dire qu'il existe $\theta$ telle que
  98   $\alpha = mgu(t,t') ; \theta$
  99 \end{itemize}
 100 \end{frame}
 101
 102 \begin{frame}
 103 \frametitle{Unification}
 104 \framesubtitle{Exercice 1}
 105 \begin{enumerate}
 106 \item Montrer que $R(h(x),y)$ et $R(z,h(a))$ sont unifiables par les
 107 substitutions suivantes
 108 \begin{itemize}
 109 \item $\sigma_1 = [z:= h(a), y:= h(a), x:=a]$
 110 \item $\sigma_2 = [z:= h(g(a,x)), y:= h(a), x:= g(a,x)]$
 111 \item $\sigma_3 = [z:= h(g(a,b)), y:= h(a),x:=g(a,b)]$
 112 \item $\sigma_4 = [z:= h(b), y:= h(a),x:=b]$
 113 \end{itemize}
 114 \item Donner $\sigma = mgu(R(h(x),y),R(z,h(a))$
 115 \item Montrer que $\sigma_1$, \ldots $\sigma_4$ sont moins générales
 116 que $\sigma$
 117 \end{enumerate}
 118 \pause
 119 \begin{itemize}
 120 \item $\sigma_1 = \sigma ; [x:=a]$
 121 \item \pause $\sigma_2 = \sigma ; [x:=g(a,x)]$
 122 \item \pause $\sigma_3 = \sigma ; [x:=g(a,b)]$
 123 \item \pause $\sigma_4 = \sigma ; [x:=b]$
 124 \end{itemize}
 125 \end{frame}
 126 %
 127 % \begin{frame}
 128 % \frametitle{Unification}
 129 % \framesubtitle{Exercice 2}
 130 % \begin{itemize}
 131 %  \item
 132 % \end{itemize}
 133 % \end{frame}