diapos/logique/.svn/text-base/resol.tex.svn-base

   1 \frame{
   2  \frametitle{Résolution propositionnelle}
   3  \framesubtitle{Principe}
   4  \begin{itemize}
   5   \item Méthode syntaxique pour caractériser les tautologies
   6   propositionnelles
   7   \item <2-> Deux étapes
   8     \begin{itemize}
   9       \item \textbf{Réduction} de la formule en CNF (\emph{Conjunctive Normal Form})
  10
  11         La formule devient un ensemble de \emph{clauses}
  12
  13       \item \textbf{Déduction} de nouvelles clauses
  14
  15         Une seule règle de déduction, appelée \emph{résolution}
  16     \end{itemize}
  17   \item <3-> (Théorème) Contradiction dans l'ensemble de clauses
  18   initial si et seulement si la clause vide en est déduite
  19   \item <4-> On dit que la méthode procède par \emph{réfutation}
  20  \end{itemize}
  21 }
  22
  23 \frame{
  24  \frametitle{Résolution propositionnelle}
  25  \framesubtitle{Forme normale conjonctive}
  26  \begin{itemize}
  27   \item Une formule propositionnelle est en CNF (\emph{Conjunctive Normal Form})
  28    si elle est de la forme $C_1 \wedge \ldots \wedge C_n$
  29    o\`u chaque $C_i$ est une clause
  30   \item <2-> Une \emph{clause} est une disjonction
  31      $L_1 \lor \ldots \lor L_k$ de litt\'eraux
  32   \item <3-> Un \emph{litt\'eral} est soit une proposition atomique $P$,
  33      soit la n\'egation $\neg P$ d'une proposition atomique
  34   \item <4-> La clause vide ($k = 0$) est notée $\bot$
  35   \item <5-> $\lor$ étant idempotent, on peut supposer tous les $L_i$ distincts, donc
  36    une clause est vue comme un ensemble de littéraux
  37   \item <6->  De même, une formule en CNF est vue comme un ensemble de clauses
  38  \end{itemize}
  39 }
  40
  41 \frame{
  42  \frametitle{Résolution propositionnelle}
  43  \framesubtitle{Réduction en CNF}
  44  \begin{itemize}
  45   \item  Appliquer le système de réécriture
  46   \begin{small}
  47   \begin{eqnarray*}
  48     F \Rightarrow G & \rightarrow & (\neg F) \lor G \\
  49     \neg (\neg F) & \rightarrow & F \\
  50     \neg (F \land G) & \rightarrow & (\neg F) \lor (\neg G) \\
  51     \neg (F \lor G) & \rightarrow & (\neg F) \land (\neg G) \\
  52     F \lor (G \land H) & \rightarrow & (F \lor G) \land (F \lor H) \\
  53     (F \land G) \lor H & \rightarrow & (F \lor H) \land (G \lor H) \\
  54     F \lor F & \rightarrow & F
  55   \end{eqnarray*}
  56   \end{small}
  57  \item<2-> Ce système termine toujours
  58 %(on peut le décomposer en systèmes plus simples dont la terminaison  est plus évidente)
  59  \item<4-> Lorsqu'aucune règle ne s'applique plus, la formule finale est en CNF
  60  \item<5-> Exemple :
  61   $B \lor C \Rightarrow A \rightarrow $ \onslide<6-> $\neg (B \lor C)
  62   \lor A$ \onslide<7->$\rightarrow$ \onslide<8->$((\neg B) \land (\neg C)) \lor A$
  63   \onslide<9->$\rightarrow$ \onslide<10->$((\neg B) \lor A) \land (\neg C) \lor A)$
  64  \end{itemize}
  65 }
  66
  67 \frame{
  68  \frametitle{Résolution propositionnelle}
  69  \framesubtitle{Règle de résolution}
  70   $$\frac{\neg P \lor C, \qquad P \lor D}{C \lor D}$$
  71    où $P$ est un atome et $C$ et $D$ sont des clauses
  72  \begin{itemize}
  73  \item <2-> Déduit une nouvelle clause de deux clauses connues
  74  \item <3-> Déduit la clause vide si $C$ et $D$ sont vides
  75  \item <4-> Si $C$ et $D$ ont des littéraux communs
  76   \begin{itemize}
  77   \item soit on les élimine par la règle de factorisation
  78     $$\frac{L \lor L \lor C}{L \lor C}$$
  79    où $L$ est un littéral et $C$ est une clause
  80   \item soit on considère les clauses comme des ensembles
  81   \end{itemize}
  82  \item <5-> On note $E \vdash C$ si la règle de résolution
  83  permet de déduire la clause $C$ de l'ensemble de clauses $E$
  84  \item<6-> Exemple :
  85   $\{p_1 \lor p_2, \neg p_2 \lor \neg p_3, p_3 \} \vdash p_1$ en deux étapes
  86  \end{itemize}
  87 }
  88
  89 \begin{frame}
  90 \frametitle{Résolution}
  91 \framesubtitle{Exercice 7.1}
  92 Soit quatre clauses $P$, $Q$, $R$ et $S$ définies par:
  93 \begin{eqnarray*}
  94 P &= & x \lor \neg y \lor \neg z \\
  95 Q &= & \neg x \lor u \\
  96 R & =& \neg y \\
  97 S & =& x \lor \neg u
  98 \end{eqnarray*}
  99 Quelles paires de clauses sont résolubles ? Dans chaque cas, quelle
 100 est la résolvante ?
 101
 102 \pause Réponse:
 103 La seule paire résoluble est $(P,Q)$
 104  et sa résolvante est $\textit{res}(P,Q) =
 105 \neg y \lor \neg z \lor u$
 106 \end{frame}
 107
 108
 109 \frame{
 110  \frametitle{Résolution propositionnelle}
 111  \framesubtitle{Théorèmes}
 112  \begin{itemize}
 113  \item Soit $\textit{cnf}(F)$ un ensemble de clauses
 114   issu de la mise en CNF de la formule $F$
 115  \item<2-> Théorème 1 : $G$ est une tautologie ($\models G$) si et seulement si
 116    $$\textit{cnf}(\neg G) \vdash \bot$$
 117  \item<3-> Théorème 2 : $H_1, \ldots, H_n \models G$ si et seulement si
 118    $$\textit{cnf}(H_1 \land \ldots \land H_n \land \neg G) \vdash \bot$$
 119  \end{itemize}
 120 }
 121
 122 \begin{frame}
 123 \frametitle{Résolution}
 124 \framesubtitle{Exercice 7.2}
 125 Montrer que
 126 $$
 127 \begin{array}{lrll}
 128 \{& C_1 = & a \lor b \lor c, &  \\
 129   & C_2 = & \neg a \lor b \lor c,& \\
 130   & C_3 = & \neg b \lor c & \} \theor c.
 131 \end{array}
 132 $$
 133
 134 \pause Réponse:
 135 on cherche à démontrer que
 136 $\{C_1,C_2,C_3,C_4 = \neg c\} \theor \bot$
 137 %ce qui revient à montrer que la résolution de cet ensemble de clauses
 138 %contient la clause vide.
 139
 140 \begin{itemize}
 141 \item \pause $C_1$ et $C_2$ sont résolubles, soit
 142 $C_5 = \textit{Res}(C_1,C_2) = \pause b \lor c $.
 143 \item \pause  $C_3$ et $C_5$ sont résolubles, soit
 144 $C_6 = \textit{Res}(C_3,C_5) = \pause  c $.
 145 \item \pause  $C_4$ et $C_6$ sont résolubles, soit
 146 $C_7 = \textit{Res}(C_3,C_5) = \pause \bot $.
 147 \end{itemize}
 148 \pause On a donc bien le résultat souhaité
 149 \end{frame}
 150
 151 % \begin{frame}
 152 % \frametitle{Résolution}
 153 % \framesubtitle{Exercice 7.3}
 154 % Démontrer à l'aide de la méthode de résolution le raisonnement
 155 % suivant:
 156 %
 157 % \begin{itemize}
 158 % \item Si Jean n'a pas rencontré Pierre l'autre nuit, c'est que Pierre
 159 %   est le meurtrier ou Jean est un menteur;
 160 % \item Si Pierre n'est pas le meurtrier, alors Jean n'a pas rencontré
 161 %   Pierre l'autre nuit et le crime a eu lieu après minuit;
 162 % \item Si le crime a eu lieu après minuit, alors Pierre est le
 163 %   meurtrier  ou Jean n'est pas un menteur.
 164 % \item Donc Pierre est le meurtrier
 165 % \end{itemize}
 166 % \end{frame}
 167 %
 168 % \begin{Exo} $ $
 169 % \begin{enumerate}
 170 % \item
 171 % Montrer que la formule suivante est  contradictoire
 172 %   $$(A \rightarrow B) \land
 173 %   (\neg A \rightarrow B \lor C) \land
 174 %   (\neg C \rightarrow \neg B) \land
 175 %   ((B \land C) \rightarrow \neg A) \land
 176 %   (C \rightarrow A)$$
 177 % \item Démontrer le théorème suivant:
 178 % $$
 179 % \{A \lor B \lor \neg D, \neg A \lor C \lor \neg D, \neg B, D \} \theor
 180 % C
 181 % $$
 182 % \end{enumerate}
 183 % \end{Exo}
 184 %