]> AND Private Git Repository - cours-maths-dis.git/blob - diapos/logique/resol.tex
Logo AND Algorithmique Numérique Distribuée

Private GIT Repository
ajout d'un cours de TS
[cours-maths-dis.git] / diapos / logique / resol.tex
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