\frame{
 \frametitle{Résolution du premier ordre et unification}
 \framesubtitle{Introduction}
 \begin{itemize}
  \item Partie II du chapitre 7 du cours  
  \item Méthode syntaxique pour détecter les formules du
  premier ordre contradictoires
  \item \pause Etapes
    \begin{itemize}
      \item 
       \textbf{Réductions} successives de la formule
       
       \begin{enumerate}
        \item \pause Mise en forme prénexe
        \item \pause Skolémisation : \pause élimination des $\exists$
        \item \pause Mise en CNF (\emph{Conjunctive Normal Form})     
       \end{enumerate}

        La formule devient un ensemble de \emph{clauses} du premier
        ordre (avec variables)

      \item \textbf{Déduction} de nouvelles clauses
 
        Deux règles de déduction : résolution et factorisation
            \end{itemize}
  \item \pause Théorème : formule initiale contradictoire
   si et seulement si la clause vide est déduite
 \end{itemize}
}

\frame{
 \frametitle{Résolution du premier ordre}
 \framesubtitle{Règles de déduction}
 \begin{itemize}
 \item Résolution
  
  $$
  \frac{a \lor \Gamma, \quad \neg b \lor \Delta}{(\Gamma \vee
  \Delta) \sigma } 
   $$


  $\sigma$ est l'unificateur le plus général de $a$ et de $b$

  \item \pause Factorisation

  $$\frac{a \ou b \ou \Gamma}{(b \ou \Gamma) \sigma}$$
  
  $\sigma$ est un unificateur de $a$ et $b$
  
  \item \pause Exemple : 
  $\{ p(x) \ou p(y) \ou q(z) \} \vdash p(y) \ou q(z)$
  car $[x := y]$ est un unificateur de $p(x)$ et $p(y)$
 \end{itemize}
}

\begin{frame}
\frametitle{Unification}
\framesubtitle{Exemple et définition}
\begin{itemize}
  \item Question : les atomes $R(h(x),y)$ et $R(z,h(a))$, où
  $x$ et $y$ sont des variables, peuvent-ils être égaux ?
  \item \pause Oui. Ils sont ``unifiables'' avec la substitution 
   $\sigma = [z:= h(x), y:= h(a)]$ car 
   
   $R(h(x),y) \sigma = $ \pause $R(h(x),h(a))$
    
   \pause et 
   
   $R(z,h(a)) \sigma = $ \pause $R(h(x),h(a))$
  \item \pause Définition : $\sigma$ est un unificateur des termes $s$
  et $t$ si $s \sigma = t \sigma$
  \item \pause Autrement dit, $\sigma$ est une solution de l'équation
   $R(h(x),y) = R(z,h(a))$  dans l'alg\`{e}bre des termes
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Unification}
\framesubtitle{}
\begin{itemize}
  \item $[z:= h(x), y:= h(a)]$ est une solution de l'équation
   $R(h(x),y) = R(z,h(a))$ 
  \item \pause Y a t'il plusieurs solutions ?
  \item \pause Oui : \pause si $\sigma$ est un unificateur,
  alors $\sigma ; \theta$ en est un aussi, pour toute substitution
  $\theta$
  \item \pause Il y a donc une infinité de solutions !
  \item Heureusement, l'équation $t = t'$ admet une solution
  minimale unique, génératrice de toutes les solutions
  \begin{itemize} 
      \item  \pause appelée ``unificateur le plus général''
      \item  \pause notée $mgu(t,t')$
      \item  \pause de support inclus dans $var(t) \cup var(t')$
  \end{itemize}
  \item \pause Toute autre solution $\alpha$ est moins générale que
  $mgu(t,t')$, c'est-à-dire qu'il existe $\theta$ telle que 
  $\alpha = mgu(t,t') ; \theta$
\end{itemize}   
\end{frame}

\begin{frame}
\frametitle{Unification}
\framesubtitle{Exercice 1}
\begin{enumerate}
\item Montrer que $R(h(x),y)$ et $R(z,h(a))$ sont unifiables par les
substitutions suivantes
\begin{itemize}
\item $\sigma_1 = [z:= h(a), y:= h(a), x:=a]$ 
\item $\sigma_2 = [z:= h(g(a,x)), y:= h(a), x:= g(a,x)]$
\item $\sigma_3 = [z:= h(g(a,b)), y:= h(a),x:=g(a,b)]$
\item $\sigma_4 = [z:= h(b), y:= h(a),x:=b]$
\end{itemize}
\item Donner $\sigma = mgu(R(h(x),y),R(z,h(a))$
\item Montrer que $\sigma_1$, \ldots $\sigma_4$ sont moins générales
que $\sigma$
\end{enumerate}
\pause
\begin{itemize}
\item $\sigma_1 = \sigma ; [x:=a]$ 
\item \pause $\sigma_2 = \sigma ; [x:=g(a,x)]$
\item \pause $\sigma_3 = \sigma ; [x:=g(a,b)]$
\item \pause $\sigma_4 = \sigma ; [x:=b]$
\end{itemize}
\end{frame}
% 
% \begin{frame}
% \frametitle{Unification}
% \framesubtitle{Exercice 2}
% \begin{itemize}
%  \item 
% \end{itemize}
% \end{frame}