\frame{
 \frametitle{Résolution propositionnelle}
 \framesubtitle{Principe}
 \begin{itemize}
  \item Méthode syntaxique pour caractériser les tautologies
  propositionnelles
  \item <2-> Deux étapes
    \begin{itemize}
      \item \textbf{Réduction} de la formule en CNF (\emph{Conjunctive Normal Form})

        La formule devient un ensemble de \emph{clauses}

      \item \textbf{Déduction} de nouvelles clauses
 
        Une seule règle de déduction, appelée \emph{résolution}
    \end{itemize}
  \item <3-> (Théorème) Contradiction dans l'ensemble de clauses
  initial si et seulement si la clause vide en est déduite
  \item <4-> On dit que la méthode procède par \emph{réfutation}
 \end{itemize}
}

\frame{
 \frametitle{Résolution propositionnelle}
 \framesubtitle{Forme normale conjonctive}
 \begin{itemize}
  \item Une formule propositionnelle est en CNF (\emph{Conjunctive Normal Form}) 
   si elle est de la forme $C_1 \wedge \ldots \wedge C_n$
   o\`u chaque $C_i$ est une clause
  \item <2-> Une \emph{clause} est une disjonction
     $L_1 \lor \ldots \lor L_k$ de litt\'eraux
  \item <3-> Un \emph{litt\'eral} est soit une proposition atomique $P$, 
     soit la n\'egation $\neg P$ d'une proposition atomique
  \item <4-> La clause vide ($k = 0$) est notée $\bot$ 
  \item <5-> $\lor$ étant idempotent, on peut supposer tous les $L_i$ distincts, donc
   une clause est vue comme un ensemble de littéraux
  \item <6->  De même, une formule en CNF est vue comme un ensemble de clauses 
 \end{itemize}
}

\frame{
 \frametitle{Résolution propositionnelle}
 \framesubtitle{Réduction en CNF}
 \begin{itemize}
  \item  Appliquer le système de réécriture 
  \begin{small}
  \begin{eqnarray*}
    F \Rightarrow G & \rightarrow & (\neg F) \lor G \\
    \neg (\neg F) & \rightarrow & F \\
    \neg (F \land G) & \rightarrow & (\neg F) \lor (\neg G) \\
    \neg (F \lor G) & \rightarrow & (\neg F) \land (\neg G) \\
    F \lor (G \land H) & \rightarrow & (F \lor G) \land (F \lor H) \\
    (F \land G) \lor H & \rightarrow & (F \lor H) \land (G \lor H) \\
    F \lor F & \rightarrow & F
  \end{eqnarray*}
  \end{small}
 \item<2-> Ce système termine toujours 
%(on peut le décomposer en systèmes plus simples dont la terminaison  est plus évidente)
 \item<4-> Lorsqu'aucune règle ne s'applique plus, la formule finale est en CNF
 \item<5-> Exemple :
  $B \lor C \Rightarrow A \rightarrow $ \onslide<6-> $\neg (B \lor C)
  \lor A$ \onslide<7->$\rightarrow$ \onslide<8->$((\neg B) \land (\neg C)) \lor A$
  \onslide<9->$\rightarrow$ \onslide<10->$((\neg B) \lor A) \land (\neg C) \lor A)$
 \end{itemize}
}

\frame{
 \frametitle{Résolution propositionnelle}
 \framesubtitle{Règle de résolution}
  $$\frac{\neg P \lor C, \qquad P \lor D}{C \lor D}$$
   où $P$ est un atome et $C$ et $D$ sont des clauses
 \begin{itemize}
 \item <2-> Déduit une nouvelle clause de deux clauses connues
 \item <3-> Déduit la clause vide si $C$ et $D$ sont vides
 \item <4-> Si $C$ et $D$ ont des littéraux communs
  \begin{itemize}
  \item soit on les élimine par la règle de factorisation
    $$\frac{L \lor L \lor C}{L \lor C}$$
   où $L$ est un littéral et $C$ est une clause
  \item soit on considère les clauses comme des ensembles
  \end{itemize}
 \item <5-> On note $E \vdash C$ si la règle de résolution
 permet de déduire la clause $C$ de l'ensemble de clauses $E$
 \item<6-> Exemple : 
  $\{p_1 \lor p_2, \neg p_2 \lor \neg p_3, p_3 \} \vdash p_1$ en deux étapes
 \end{itemize}
}

\begin{frame}
\frametitle{Résolution}
\framesubtitle{Exercice 7.1}
Soit quatre clauses $P$, $Q$, $R$ et $S$ définies par:
\begin{eqnarray*}
P &= & x \lor \neg y \lor \neg z \\
Q &= & \neg x \lor u \\
R & =& \neg y \\
S & =& x \lor \neg u 
\end{eqnarray*}
Quelles paires de clauses sont résolubles ? Dans chaque cas, quelle
est la résolvante ?

\pause Réponse:
La seule paire résoluble est $(P,Q)$
 et sa résolvante est $\textit{res}(P,Q) = 
\neg y \lor \neg z \lor u$
\end{frame}


\frame{
 \frametitle{Résolution propositionnelle}
 \framesubtitle{Théorèmes}
 \begin{itemize}
 \item Soit $\textit{cnf}(F)$ un ensemble de clauses
  issu de la mise en CNF de la formule $F$
 \item<2-> Théorème 1 : $G$ est une tautologie ($\models G$) si et seulement si
   $$\textit{cnf}(\neg G) \vdash \bot$$
 \item<3-> Théorème 2 : $H_1, \ldots, H_n \models G$ si et seulement si
   $$\textit{cnf}(H_1 \land \ldots \land H_n \land \neg G) \vdash \bot$$
 \end{itemize}
}

\begin{frame}
\frametitle{Résolution}
\framesubtitle{Exercice 7.2}
Montrer que 
$$
\begin{array}{lrll}
\{& C_1 = & a \lor b \lor c, &  \\
  & C_2 = & \neg a \lor b \lor c,& \\
  & C_3 = & \neg b \lor c & \} \theor c.
\end{array}  
$$

\pause Réponse:
on cherche à démontrer que 
$\{C_1,C_2,C_3,C_4 = \neg c\} \theor \bot$
%ce qui revient à montrer que la résolution de cet ensemble de clauses
%contient la clause vide.

\begin{itemize}
\item \pause $C_1$ et $C_2$ sont résolubles, soit 
$C_5 = \textit{Res}(C_1,C_2) = \pause b \lor c $.
\item \pause  $C_3$ et $C_5$ sont résolubles, soit 
$C_6 = \textit{Res}(C_3,C_5) = \pause  c $.
\item \pause  $C_4$ et $C_6$ sont résolubles, soit 
$C_7 = \textit{Res}(C_3,C_5) = \pause \bot $.
\end{itemize}
\pause On a donc bien le résultat souhaité
\end{frame}

% \begin{frame}
% \frametitle{Résolution}
% \framesubtitle{Exercice 7.3}
% Démontrer à l'aide de la méthode de résolution le raisonnement
% suivant:
% 
% \begin{itemize}
% \item Si Jean n'a pas rencontré Pierre l'autre nuit, c'est que Pierre
%   est le meurtrier ou Jean est un menteur;
% \item Si Pierre n'est pas le meurtrier, alors Jean n'a pas rencontré
%   Pierre l'autre nuit et le crime a eu lieu après minuit;
% \item Si le crime a eu lieu après minuit, alors Pierre est le
%   meurtrier  ou Jean n'est pas un menteur.
% \item Donc Pierre est le meurtrier
% \end{itemize}
% \end{frame}
% 
% \begin{Exo} $ $
% \begin{enumerate}
% \item 
% Montrer que la formule suivante est  contradictoire
%   $$(A \rightarrow B) \land 
%   (\neg A \rightarrow B \lor C) \land 
%   (\neg C \rightarrow \neg B) \land 
%   ((B \land C) \rightarrow \neg A) \land 
%   (C \rightarrow A)$$
% \item Démontrer le théorème suivant:
% $$
% \{A \lor B \lor \neg D, \neg A \lor C \lor \neg D, \neg B, D \} \theor
% C
% $$
% \end{enumerate}
% \end{Exo}
%