%% Time-stamp: <modified on 13 Dec 2004 at 15:26 by Pierre Lescanne>
%% /MIM-1/REECRITURE/UNIFICATION/unif.tex
\documentclass[%
  slidesonly,%  Pour sortir les transparents seuls
  semrot,%      Permettre des rotations eventuelles
  semhelv,%    Helvetica
  a4%           A4 paper
  ]{seminar}

\def\printlandscape{\special{landscape}}     % pour sortir en landscape
\slidesmag{5}

\usepackage{amsfonts,amsmath,amsthm,amssymb,stmaryrd}
\usepackage{fancybox}
\usepackage[francais]{babel}
\usepackage[latin1]{inputenc}
\usepackage{color}
%\usepackage{amsmath}
\usepackage[all]{xy}
\usepackage{qsymbols}
\usepackage{prooftree}
\usepackage[dvips]{graphicx}

%% Time-stamping  
%% compute the time in hours and minutes; 
 \newcount\timehh\newcount\timemm \timehh=\time 
 \divide\timehh by 60 \timemm=\time
 \count255=\timehh\multiply\count255 by -60 \advance\timemm by \count255
 \newcommand{\timestamp}
 { {\protect\small\sl\today\ -- 
 \ifnum\timehh<10 0\fi\number\timehh\,h\,
   \ifnum\timemm<10 0\fi\number\timemm}}
                                          % avec dvips


\articlemag{1}

\rotateheaderstrue       % si tu combines slide et slide*

\title{\color{red}{\textit{Réécriture}}}

\author{La résolution}

\date{}

\pagestyle{}

\slidestyle{empty}

\slideframe{}   

%--- couleurs ----
\input{mes_couleurs}

%--- symboles ---
\renewcommand{\phi}{\varphi}
%\newcommand{\llbracket}{\ensuremath{|\![}}
%\newcommand{\rrbracket}{\ensuremath{]\!|}}
\newcommand{\Emb}{\bl{\ensuremath{\cal EMB}}}
\newcommand{\ali}{\newline\hspace*{18pt}}
\newcommand{\shat}{\ensuremath{\hat{\sigma}}}
\newcommand{\pref}{\mathop{\textbf{\textsl{prefix}}}}
\newcommand{\IN}{\ensuremath{\mathcal{IN}}}
\newcommand{\gtmult}{\ensuremath{>_{mult}}}
\newcommand{\dminus}{\mbox{\ensuremath{\stackrel{\raisebox{+.01ex}{.}}{-}}}}
%\newcommand{\Nat}{\textsf{I}\hspace{-.7pt}\textsf{N}}
\newcommand{\Nat}{\mathbb{N}}
\newcommand{\Natstar}{\Nat_\star}
\newcommand{\A}{\ensuremath{\bl{\cal A}}}
\newcommand{\M}{{\cal M}}
\newcommand{\U}{{\cal U}}
\newcommand{\calC}{\ensuremath{\cal C}}
\newcommand{\Ra}{\ensuremath{\mathop{\Rightarrow}}}
\newcommand{\et}{\mathop{\&}}
\newcommand{\sh}{\mathop{|}}
\newcommand{\set}[2]{\{#1~|~#2\}}
\newcommand{\da}{\downarrow}
\newcommand{\jgbl}{\mathop{\da}}
\newcommand{\lpo}{<_{lpo}}
\newcommand{\lepo}{\le_{lpo}}
\newcommand{\eq}{\stackrel{?}{=}}
\newcommand{\mere}[2]{\bl{\textrm{mère(\brunir{#1},\brunir{#2})}}}
\newcommand{\pere}[2]{\bl{\textrm{père(\brunir{#1},\brunir{#2})}}}

\newcommand{\inferTwoLabel}[4]{\bl{
 {#1} \quad 
 \begin{array}{c}
   #2 \hspace{2em} #3\\
   \hline \noalign{\vskip 1pt}#4
  \end{array}}}

\newcommand{\leafLabel}[2]{\bl{
 {#1} \quad
  \begin{array}{c}
  #2
  \end{array} }}


%\newcommand{\inferLabel}[3]{\emph{#1}\ali #2 \Mapsto #3}

\newcommand{\inferLabel}[3]{
    \rouge{#1} \quad 
    \bl{\begin{array}{c}
      #2\\
      \hline \noalign{\vskip 1pt}#3
    \end{array}
  }}

\newenvironment{eqnarraybleu}%
  {\begin{color}{blue}\begin{eqnarray*}}
  {\end{eqnarray*}\end{color}}

\newenvironment{displaymathbleu}[1]{\begin{displaymath}\color{blue}#1}{\end{displaymath}}

\newenvironment{mathbleu}[1]{\begin{math}\color{blue}#1}{\end{math}}
  
% I rename the bullet which starts itemize list to avoid bullets;
\renewcommand{\labelitemi}{\(\star\)}

%% ==============================================================
%%                   Reductions and other relations
%% ==============================================================

\newcommand{\ra}{\xymatrix @C 15pt {\ar@{>}[r] &}}
\newcommand{\ranorm}{\xymatrix @C 15pt {\ar@{>>|}[r] &}}
\newcommand{\rara}{\xymatrix @C 15pt {\ar@{>>}[r] &}}
\newcommand{\longequiv}{\xymatrix @C 15pt {\ar@3{-}[r] &}}

%%%%%%%%%%%%%%%%%%%% iteration of arrows  %%%%%%%%%%%%%%%%%%%%
\newcommand{\rastar}{\rasup{*}}
\newcommand{\raplus}{\rasup{+}}

%%%%%%%%%%%%%%%%%%%% fleches avec souscrit et superscrit %%%%%%%%%%%%%
% par exemple -- B, p --> s'ecrit \rasub{B,p}

\newcommand{\rasub}[1]{\xymatrix @C 15pt {\ar@{>}[r]_{#1} &}}
\newcommand{\subar}[1]{\xymatrix @C 15pt {\ar@{<-}[r]_{#1} &}}
\newcommand{\ranormsub}[1]{\xymatrix @C 15pt {\ar@{>>|}[r]_{#1} &}}
\newcommand{\rarasub}[1]{\xymatrix @C 15pt {\ar@{>>}[r]_{#1} &}}
\newcommand{\rasup}[1]{\xymatrix @C 15pt {\ar@{>}[r]^{#1} &}}
\newcommand{\supar}[1]{\xymatrix @C 15pt {\ar@{<-}[r]^{#1} &}}
\newcommand{\rarasup}[1]{\xymatrix @C 15pt {\ar@{>>}[r]^{#1} &}}
\newcommand{\rasupsub}[2]{\xymatrix @C 15pt {\ar@{>}[r]^{#1}_{#2} &}}
\newcommand{\rarasupsub}[2]{\xymatrix @C 15pt {\ar@{>>}[r]^{#1}_{#2} &}}
\newcommand{\cv}[1]{\xymatrix @C 20pt {\ar@{<->}[r]_{#1} &}}
\newcommand{\conv}[1]{\xymatrix @C 20pt {\ar@{<->}[r]_{#1}^{*} &}}
\newcommand{\convplus}[1]{\xymatrix @C 20pt {\ar@{<->}[r]_{#1}^{+} &}}

%%%%%%%%%%%%%%%%%%%% Les fleches %%%%%%%%%%%%%

\newcommand{\rabeta}{\rasub{\beta}}
\newcommand{\rarabeta}{\rarasub{\beta}}
\newcommand{\raE}{\rasub{E}}
\newcommand{\raR}{\rasub{R}}
\newcommand{\Rar}{\subar{R}}
\newcommand{\rastarR}{\rasupsub{*}{R}}
\newcommand{\raraR}{\rarasub{R}}
\newcommand{\plusararR}{\xymatrix{&\ar@{>>}[l]^{R}_+}}
\newcommand{\plusraraR}{\rarasupsub{+}{R}}
\newcommand{\rapar}{\xymatrix @ -1.5pc {\ar@{>}[rr]&||&}}
\newcommand{\rarapar}{\xymatrix @ -1.5pc {\ar@{>>}[rr]&||&}}
\newcommand{\remb}{\rasub{\Emb}}
\newcommand{\plgt}{\rasupsub{+}{\Emb}}
\newcommand{\plonge}{\xymatrix{\ar@{<-}[r]_{\Emb}^{*} &}}

%%%%%%%%%%%%%%%%% Headings %%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\heading}[1]{%
{\color{cyanp}\textbf{\large #1}}{\color{yellow}\\\rule{\textwidth}{2pt}
}}

%\newcommand{\heading}[1]{%      % ca c'est des commandes a moi
%  \begin{center}                % mais ca peut t'interesser
%    \large\bf
%    \color{cyan}{\shadowbox{#1}}%
%  \end{center}
%  \markright{#1}
%  \vspace{1ex minus 1ex}}

\newcommand{\subheading}[1]{%
  \begin{center}
    \color{vertfonce}{\bf\Ovalbox{#1}}
  \end{center}}

\begin{document}
%------------------------------------------------------
\begin{slide}
    \maketitle
    \addtocounter{slide}{-1}
    \slidepagestyle{empty}


\bigskip
\bigskip

\begin{quotation}
  \verdir{\noindent Il faut tenir à une résolution parce qu'elle est
    bonne, \\ et non parce qu'on l'a prise.}

\hfill\textit{La Rochefoucauld}
\end{quotation}

\vfill 
\hfill\textit{\footnotesize version du \timestamp}

\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{La résolution en calcul propositionnel}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La règle  cut}
En calcul des séquents, la \emph{coupure} (ou \emph{cut}) est la règle

\begin{displaymathbleu}
  \prooftree
  A, `G"|-" `D \qquad `X "|-"A,`Q
  \justifies `G, `X "|-" `D, `Q
  \endprooftree
\end{displaymathbleu}
ce qui donne aussi
\begin{displaymathbleu}
  \prooftree
  A, A_1,\ldots,A_m "|-" B_1,\ldots,B_n \qquad \qquad C_1,\ldots,C_p"|-"A, D_1,\ldots,D_q
  \justifies A_1,\ldots,A_m, C_1,\ldots,C_p "|-" B_1,\ldots,B_n, D_1,\ldots,D_q
  \endprooftree
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Interprétation des séquents}
Le séquent 
\begin{displaymathbleu}
  A_1,\ldots,A_m "|-" B_1,\ldots,B_n
\end{displaymathbleu}
s'interprète par 
\begin{displaymathbleu}
  A_1`^\ldots`^A_m "=>"  B_1`V\ldots `V B_n
\end{displaymathbleu}
ou encore
\begin{displaymathbleu}
  `!A_1`V\ldots`V`!A_m `V B_1 `V\ldots `V B_n
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Introduction à la résolution en calcul propositionnel}
Si on récrit \emph{cut} dans cette interprétation
\begin{scriptsize}
\begin{displaymathbleu}
  \prooftree
  `!A`V`! A_1`V\ldots `V`!A_m `V B_1 `V\ldots `V B_n \qquad \qquad %
  A `V `!C_1`V`! \ldots`V`! C_p `V D_1 \ldots `V D_q %
  \justifies `!  A_1,\ldots`V`! A_m `V C_1,\ldots `V C_p `V B_1 `V
  \ldots `V B_n `V D_1 `V \ldots `V D_q \endprooftree
\end{displaymathbleu}
\end{scriptsize}
ou encore si \bleu{`F} et \bleu{`J} sont des disjonctions de
propositions
\begin{displaymathbleu}
  \prooftree %
  `!A`V`F \qquad \qquad A `V `J %
  \justifies `F `V `J 
 \endprooftree
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Introduction à la résolution en calcul propositionnel}
Si on récrit \emph{cut} dans cette interprétation
\begin{scriptsize}
\begin{displaymathbleu}
  \prooftree
  `!A`V`! A_1`V\ldots `V`!A_m `V B_1 `V\ldots `V B_n \qquad \qquad %
  A `V `!C_1`V`! \ldots`V`! C_p `V D_1 \ldots `V D_q %
  \justifies `!  A_1,\ldots`V`! A_m `V C_1,\ldots `V C_p `V B_1 `V
  \ldots `V B_n `V D_1 `V \ldots `V D_q \endprooftree
\end{displaymathbleu}
\end{scriptsize}
ou encore si \bleu{`F} et \bleu{`J} sont des conjonctions de
propositions
\begin{displaymathbleu}
  \prooftree %
  `!A`V`F \qquad \qquad A `V `J %
  \justifies `F `V `J 
 \endprooftree
\end{displaymathbleu}
\vfill La spécificité de la résolution (en calcul propositionnel) est
que \emph{tous les \bleu{A_i} sont des variables propositionnelles}.
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La résolution en calcul propositionnel}
La résolution
\begin{displaymathbleu}
  \prooftree %
  `!A`V`F \qquad \qquad A `V `J %
  \justifies `F `V `J 
 \endprooftree
\end{displaymathbleu}
est apparentée à notre bon vieux modus ponens

car on peut l'écrire
\begin{displaymathbleu}
  \prooftree %
  A "=>" `F \qquad \qquad A `V `J %
  \justifies `F `V `J 
 \endprooftree
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Formes clausales} %
  Pour la résolution on travaille sur les propositions mises\\ sous
  \emph{forme normale conjonctive},

c'est-à-dire sous la forme de \verdir{conjonction de disjonctions} de
\emph{littéraux}.

Un \emph{littéral} est 
\begin{itemize}
\item soit une \verdir{variable propositionnelle},
\item soit la \verdir{négation d'une variable propositionnelle}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Formes clausales} %
Une \verdir{forme clausale} est donc une expression de la forme
\begin{displaymathbleu}
  \bigwedge_{i=1}^n (\bigvee_{j=1}^{p_i} A_{i\,j} \vee \bigvee_{j=1}^{q_i} `!B_{i\,j})
\end{displaymathbleu}
où les \bleu{A_{i\,j}} et les  \bleu{B_{i\,j}} sont des variables
    propositionnelles.

\bleu{A_{i\,j}} est un \emph{littéral positif}.
\hfill
\bleu{`!B_{i\,j}} est un \emph{littéral négatif}.

Chaque \bleu{\bigvee_{j=1}^{p_i} A_{i\,j} \vee \bigvee_{j=1}^{q_i}
  `!B_{i\,j}} est appelé une \emph{clause}.
\vfill
Une forme clausale est donc vue comme un \emph{ensemble de clauses}.

De même, une clause peut-être vue comme un \emph{ensemble de littéraux}.
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La résolution} %
Une \emph{étape de résolution} consiste donc 
\begin{itemize}
\item à identifier un littéral \bleu{A} dans une clause \bleu{A`V`F}
\item à identifier son opposé  \bleu{`!A} dans une clause \bleu{`!A`V`J}
\end{itemize}
et à fabriquer un \emph{résolvant} \bleu{`F`V`J}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Exemples de résolution} %
La clause \bleu{\{A, B\}} et la clause  \bleu{\{`!A, `!B\}} ont
deux résolvants

\qquad \bleu{\{A, `!A\}} 

\qquad et \bleu{\{B, `!B\}}.


\vspace*{20pt}

La clause \bleu{\{C\}} et la clause  \bleu{\{`!C\}} ont un seul
résolvant \ali la \emph{clause vide} que l'on note \bleu{`[]}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Exemples de résolution} %
La clause \bleu{\{A, B\}} et elle-même ont deux résolvants:

\qquad \bleu{\{A, `!A\}} 

et \qquad \bleu{\{A, `!A\}} 

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Exemples de résolution} %
La clause \bleu{\{A, `!A\}} et elle-même ont deux résolvants:

\qquad \bleu{\{A, `!A\}} 

et \qquad \bleu{\{A, `!A\}} 

\vfill
\emph{On n'a pas beaucoup progressé!}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La procédure de résolution} %
La procédure de résolution consiste à enrichir un ensemble de clauses
par leurs résolvants jusqu'à ce qu'on engendre la clause vide.

\vspace*{20pt} 

\includegraphics[width=1cm]{attention.eps} \hspace*{20pt}\parbox{5,5cm}{Quand on ajoute le
résolvant de \bleu{`F} et \bleu{`J}, \ali on ne supprime ni \bleu{`F} ni
\bleu{`J}.}

\vspace*{20pt} 

En effet, après résolution, on doit obtenir un ensemble de clauses
logiquement équivalent.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Preuve par réfutation} %
  Quand on veut prouver une proposition,
  \begin{itemize}
  \item on prend sa \emph{négation} 
  \item on la met sous \emph{forme clausale},
  \item on prouve par résolution que cette forme clausale est
    \emph{contradictoire}.
\end{itemize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Preuve par réfutation et par résolution} %
\emph{donnée :} \bleu{S} un ensemble de clauses

\emph{répéter} 

\hspace*{20pt}\emph{choisir} \bleu{`F_1} et \bleu{`F_2} qui ont un
résolvant \bleu{`J}.

\hspace*{20pt}\bleu{S:= S \cup \{`J\}}

\emph{jusqu'à} \bleu{`J = `[]}


\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Preuve par réfutation et par résolution} %
  La mise en {\oe}uvre de la procédure de choix est une clé de
  l'implantation.  
  
  Cela correspond au parcours «astucieux» d'un graphe.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le graphe de résolution} %
  Le \emph{graphe de résolution} d'un ensemble \bleu{\cal{E}} de
  clauses est un graphe orienté sans cycle (DAG) étiqueté par des clauses
\begin{itemize}
\item dont les étiquettes des feuilles sont les clauses de  \bleu{\cal{E}},
\item chaque n{\oe}ud est étiqueté par une clause \bleu{`F} et est
  issu de deux autres n{\oe}uds étiquetés par deux clauses \bleu{`F_1}
  et \bleu{`F_2}, et \bleu{`F} est un résolvant de \bleu{`F_1} et
  \bleu{`F_2}.
\end{itemize}
\vfill Si la racine du graphe sans cycle est étiquetée par la clause
vide \bleu{`[]} \ali on dit qu'il s'agit d'une \emph{réfutation par
résolution} de l'ensemble \bleu{\cal{E}}.
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Un exemple de graphe de résolution} %
  \begin{displaymathbleu}
\xymatrix @C 3pt @R 20pt{%
  \{A, B\} \ar@{-}[dr] \ar@{-}[drrr] && \{A, `!B\}\ar@{-}[dl]  && \{`!A, B\} \ar@{-}[dl] && \{`!A, `!B\}\ar@{-}[ddl] \\
  & \{A\} \ar@{-}[ddrr]&& \{B\} \ar@{-}[drr]\\
  &&&&&\{`!A\}\ar@{-}[dll] \\
&&&`[]%
}
\end{displaymathbleu}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Insatisfiabilité} %
Une formule \bleu{`f} est \emph{insatisfiable} s'il n'existe aucune
interprétation \bleu{\mathfrak{I}} telle que 
\bleu{\mathfrak{I} "|="_K `f} 
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Correction} %
Si un ensemble \bleu{\cal{E}} de clauses admet une réfutation par
résolution alors il est insatisfiable 
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Complétude} %
  \fbox{\parbox{8cm}{Si une ensemble \bleu{\cal{E}} de clauses est
      insatisfiable alors il admet une réfutation par résolution.}}
  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Complétude} %
  \fbox{\parbox{8cm}{Si une ensemble \bleu{\cal{E}} de clauses est
      insatisfiable alors il admet une réfutation par résolution.}}

\medskip

\emph{Idée de la démonstration :}\\
On note l'analogie entre un séquent
\begin{displaymathbleu}
  A_1,\ldots, A_m "|-" B_1,\ldots, B_n
\end{displaymathbleu}
où toutes les propositions qui interviennent sont des variables
propositionnelles, et la clause
\begin{displaymathbleu}
 `! A_1 `V \ldots `V `!A_m `V B_1 `V\ldots, `V B_n
\end{displaymathbleu}
\end{slide}
%------------------------------------------------------
\begin{slide}
Considérons l'arbre d'affectation des variables propositionnelles qui définit toutes les interprétations.
\begin{displaymathbleu}
  \xymatrix @C 15pt {
&&&& &&&& &&&&& \\
&\ar@{.}[ul]^{C}\ar@{.}[ur]_{`!C}&&&&\ar@{.}[ul]^{C}\ar@{.}[ur]_{`!C}&&&\ar@{.}[ul]^{C}\ar@{.}[ur]_{`!C}&&&&\ar@{.}[ul]^{C}\ar@{.}[ur]_{`!C}\\
&&&\ar@{-}[ull]^{B}\ar@{-}[urr]_{`!B}&&&&&&&\ar@{-}[ull]^{B}\ar@{-}[urr]_{`!B}\\
& &&&&&&  \ar@{-}[ullll]^{A}\ar@{-}[urrr]_{`!A}
}
\end{displaymathbleu}
On voit que chaque branche est recouverte par une affectation qui ne satisfait pas l'une des clauses de \bleu{\cal{E}}.

Si ce n'était pas le cas,  \bleu{\cal{E}} serait satisfiable.
  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  Ainsi si l'on traduit cela en calcul des séquents, on voit que l'arbre d'affectation des variables propositionnelles
  devient un arbre de preuve en calcul des séquents,
  \begin{itemize}
  \item dont la racine est le séquent \bleu{"|-"},
  \item dont le feuilles sont des clauses de \bleu{\cal{E}}.
  \end{itemize}
\vfill
  Donc si \bleu{\cal{E}} est insatisfiable, il y a un arbre de preuve de \bleu{"|-"} dans le calcul des séquents où l'on
  utilise que la règle de coupure
\begin{displaymathbleu}
  \prooftree A, `G"|-" `D \qquad `X "|-"A,`Q %
  \justifies `G, `X "|-" `D, `Q \endprooftree
\end{displaymathbleu}
et où l'on utilise comme axiome les différentes clauses de l'ensemble~\bleu{\cal{E}}.
\end{slide}
%------------------------------------------------------
\begin{slide}
Étant donné une arbre de preuve, on lui associe le graphe sans cycle
qui correspond à la fusion maximum des preuves des séquents
identiques.

\emph{Par exemple}
\begin{displaymathbleu}
   \prooftree %
  \prooftree %
 "|-" A,B  \qquad  B "|-" A
\justifies  "|-" A
  \endprooftree %
\qquad
  \prooftree %1
  \prooftree %2
 A "|-" B \qquad A, B "|-"   %
 \justifies "|-" B
 \endprooftree %2
 \qquad%
 A,B"|-"%
\justifies A"|-"
 \endprooftree %1
\justifies "|-"
 \endprooftree %1
 \end{displaymathbleu}

  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
Étant donné une arbre de preuve, on lui associe le graphe sans cycle
qui correspond à la fusion maximum des preuves des séquents
identiques.

\emph{Par exemple}
\begin{displaymathbleu}
   \prooftree %
  \prooftree %
"|-" A,B  \qquad  B "|-" A
\justifies  "|-" A
  \endprooftree %
\qquad
  \prooftree %1
  \prooftree %2
A "|-" B \qquad \emph{\Ovalbox{\bleu{A, B "|-" }}}  %
 \justifies "|-" B
 \endprooftree %2
 \qquad%
 \verdir{\Ovalbox{\bleu{A, B "|-" }}}%
\justifies A"|-"
 \endprooftree %1
\justifies "|-"
 \endprooftree %1
 \end{displaymathbleu}

  \vfill
On «fusionne» dans l'arbre de preuve les branches correspondant à la
même sous-preuve. On crée un graphe de preuves sans cycle.
\end{slide}
%------------------------------------------------------
\begin{slide}
Étant donné une arbre de preuve, on lui associe le graphe sans cycle
qui correspond à la fusion maximum des preuves des séquents
identiques.

\emph{Par exemple}
\begin{displaymathbleu}
   \prooftree %
  \prooftree %
B "|-" A \qquad "|-" A,B
\justifies  "|-" A
  \endprooftree %
\qquad
  \prooftree %1
  \prooftree %2
A "|-" B \qquad \emph{\Ovalbox{\bleu{A, B "|-" }}}  %
 \justifies "|-" B
 \endprooftree %2
 \qquad%
\verdir{\Huge \bullet}
\justifies A"|-"
 \endprooftree %1
\justifies "|-"
 \endprooftree %1
 \end{displaymathbleu}

  \vfill
On «fusionne» dans l'arbre de preuve les branches correspondant à la
même sous-preuve. On crée un graphe de preuves sans cycle.
\end{slide}
%------------------------------------------------------
\begin{slide}
  On montre qu'il y a une correspondance entre les \emph{arbres de preuves}
  du calcul de séquents et les \emph{graphes de résolution}.

\vspace*{40pt}

Autrement dit, \verdir{si un ensemble de clauses est insatisfiable%
\ali il existe une réfutation par résolution.}
\vfill%
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{La résolution en calcul des
          prédicats du premier ordre}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Formes prénexes} %
Une formule est en \emph{forme prénexe}, \textbf{si}
\begin{itemize}
\item elle ne contient aucun quantificateur,
\item ou bien elle est de forme \bleu{Q_1 x_1\ldots Q_n x_n B} où
  \begin{itemize}
  \item \bleu{B} est une formule sans quantificateurs, 
  \item \bleu{x_1}, \ldots, \bleu{x_n} sont des variables
  \item et \bleu{Q_i\in \{`A,`E\}} pour \bleu{i=1,\ldots,n}.
\end{itemize}
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Formes prénexes} %
\fbox{\parbox{8cm}{Pour toute formule \bleu{`F}, il existe une formule
    \bleu{`J} en forme prénexe telle que \bleu{`F"<=>"`J}.}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Exercice} %
Mettre les formules suivantes en forme prénexe:

\bleu{(`!`A x P(x)) "=>" `A y Q(y)}

\bleu{`A x (`A y Q(x,y) "=>" P(x))}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Skolémisation} %
La \emph{Skolémisation} ou \emph{mise en forme de Skolem} consiste à
supprimer les quantificateurs de la façon suivante.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Skolémisation} %
On considère le quantificateur le plus profond.

\begin{itemize}
\item Si ce quantificateur est un \emph{quantificateur universel}, on le
  supprime et on transforme la variable quantifiée en une variable
  libre.

\qquad \bleu{Q_1 x_1\ldots Q_n x_n `A x P(x_1,\ldots, x_n, x)} 

\qquad \qquad donne 

\qquad \bleu{Q_1
  x_1\ldots Q_n x_n P(x_1,\ldots, x_n, x)}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Skolémisation} %

\begin{itemize}
\item Si ce quantificateur est un \emph{quantificateur existentiel}, on
  remplace toutes les occurrences des variables associées à ce
  prédicat par un symbole de fonction qui dépend de toutes les
  variables quantifiées universellement qui précèdent.
  
  \qquad \bleu{Q_1\ x_1 \ldots Q_n x_n `E x P(x_1,\ldots, x_n, x)} 

  \qquad \qquad donne 

  \qquad \bleu{Q_1
    x_1\ldots Q_n x_n P(x_1,\ldots, x_n, f(x_{j_1}, \ldots, x_{j_q}))} %

  \qquad où les \bleu{x_{j_1}, \ldots, x_{j_q}} sont les variables
  correspondant \ali aux quantificateurs universels.

\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Skolémisation} %
  \qquad \bleu{`A x_1 `E x_2 `A x_3 `E x_4 R(x_1,x_2,x_3,x_4) } 

  \qquad \qquad donne 

  \qquad \bleu{R(x_1,g(x_1),x_3,f(x_1,x_3))}.

\medskip

Les fonctions \bleu{f} et \bleu{g} introduites s'appellent les
\emph{fonctions de Skolem}.

\bigskip
  
  \brunir{Petit truc}\\
  Lors de la mise en forme prénexe (qui précède a priori la
  skolémisation), on doit éviter de «sortir» les quantificateurs
  universels avant les quantificateurs existentiels, pour ne pas
  augmenter inutilement l'arité des fonctions de Skolem.  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Skolémisation} %
\fbox{\parbox{8.7cm}{Une proposition est satisfiable si et seulement si
    sa forme skolémisée est satisfiable.}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Littéraux} %
%
Un \emph{littéral} est une formule de la forme 
\begin{itemize}
\item soit \bleu{P(t_1,...,t_k)},
\item soit \bleu{`!P(t_1,...,t_k)},
\end{itemize}
où \bleu{P(t_1,...,t_k)} est un atome, autrement dit \bleu{P} est un
symbole de prédicats et \bleu{t_1}, ..., \bleu{t_k}, sont des termes.

\bigskip

On écrira \bleu{L(x_1,...,x_m)} et \bleu{`!L(x_1,...,x_m)} %
\ali où \bleu{FV(L(x_1,...,x_m)) = \{x_1,...,x_m\}}, %
\ali et où \bleu{L(x_1,...,x_m)} est un littéral positif ne commençant
pas par le signe \bleu{`!}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Mise sous forme clausale} %
Étant donnée une formule du calcul des prédicats, la \emph{mise sous
  forme clausale} consiste 
\begin{enumerate}
\item à mettre la formule sous forme prénexe,
\item à skolémiser la formule prénexe,
\item à mettre la skolémisée sous forme clausale.
\end{enumerate}
\vfill
 C'est la phase préparatoire à la résolution.
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Mise sous forme clausale} %
  La forme clausale de la formule 
  \begin{displaymathbleu}
    `A x (`A y Q(x,y) "=>" P(x))
\end{displaymathbleu}
  est la formule
  \begin{displaymathbleu}
    P(x) `V `! Q(x,f(x))
  \end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Mise sous forme clausale} %
Soit la proposition
\begin{quote}
  \textit{Toute relation irréflexive et transitive est antisymétrique}
\end{quote}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Mise sous forme clausale} %
  Sans tenir compte de la caractérisation de l'identité, cela s'énonce
  par la formule
 \begin{eqnarraybleu}
  (`A x~`!R(x,x)) &`^& `A y `A z `A u (R(y,z) ~`^~ R(z,u) "=>" R(y,u))))\\ %
  &"=>"& `A v `A w (R(v,w) ~`^~ R(w,v) "=>" (v = w))
  \end{eqnarraybleu}
dont la négation  est
  \begin{eqnarraybleu}
  `![(`A x~`!R(x,x)) &`^& `A y `A z `A u (R(y,z) ~`^~ R(z,u) "=>" R(y,u))))\\ %
  &"=>"& `A v `A w (R(v,w) ~`^~ R(w,v) "=>" (v = w))]
  \end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
qui a pour forme prénexe
\begin{eqnarraybleu}
  `E v`E w`A x`A y `A z `A u ~`![`!R(x,x) ~`^~ (R(y,z) ~`^~ R(z,u) "=>" R(y,u))]\\ %
 \qquad  "=>" (R(v,w) ~`^~ R(w,v) "=>" (v=w))]
\end{eqnarraybleu}

Cette négation a pour formule skolémisée
\begin{eqnarraybleu}
  `![(`!R(x,x)) &`^& (R(y,z) ~`^~ R(z,u) "=>" R(y,u))))\\ %
  &"=>"& (R(a,b) ~`^~ R(b,a) "=>" (a=b))]
\end{eqnarraybleu}
où \bleu{a} et \bleu{b} sont de nouvelles constantes.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Mise sous forme clausale} %
Puis elle a pour forme clausale
\begin{eqnarraybleu}
  `!R(x,x) &`^& (`!R(y,z) `V `!R(z,u) `V R(y,u))\\ %
  &`^& R(a,b) ~`^~ R(b,a) ~`^~ `!(a=b).
\end{eqnarraybleu}

Elle correspond à l'ensemble de clauses
\begin{footnotesize}
\begin{displaymathbleu}
  S = \{`!R(x,x),\quad`!R(y,z) `V `!R(z,u) `V R(y,u),\quad
  R(a,b),\quad R(b,a),\quad `!(a=b)\}.
\end{displaymathbleu}
\end{footnotesize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Résolution} %
%
La règle de résolution s'applique à des clauses.

Elle s'énonce ainsi:

  \begin{displaymathbleu}
  \prooftree %
  `!L(x_1,...,x_m)`V`F \qquad \qquad L'(y_1,...,y_n) `V `J %
  \justifies `s(`F) `V `s(`J) %
    \endprooftree
\end{displaymathbleu}

\begin{center}
  où \bleu{`s = mgu(L(x_1,...,x_m), L'(y_1,...,y_n))}.
\end{center}

Autrement dit, \bleu{`s} est l'unificateur le plus général \ali de \bleu{ L(x_1,...,x_m)} et \bleu{L'(y_1,...,y_n)}. 
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{brunfonce}{\textit{Un exemple}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\vspace*{-20pt}
\begin{footnotesize}
\begin{eqnarraybleu}
  S_0 &=& \{\emph{`!R(x,x)},\quad`!R(y,z) `V `!R(z,u) `V \verdir{R(y,u)},\quad
  R(a,b),\quad R(b,a),\\
  &&\quad `!(a=b)\}
\end{eqnarraybleu}
avec \bleu{`s_1 = \{y "|->" x,\quad u "|->" x\}},
\begin{eqnarraybleu}
  S_1 &=& \{`!R(x,x),\quad`!R(y,z) `V `!R(z,u) `V R(y,u),\quad
  \verdir{R(a,b)},\quad R(b,a),\\ % 
  && `!(a=b),\quad \emph{`!R(x,z)} `V  `!R(z,x)\}
\end{eqnarraybleu}
avec \bleu{`s_2 = \{x "|->" a,\quad z "|->" b\}},
\begin{eqnarraybleu}
  S_2 &=& \{`!R(x,x),\quad`!R(y,z) `V `!R(z,u) `V R(y,u),\quad
  R(a,b),\quad \verdir{R(b,a)},\\ % 
  && `!(a=b),\quad `!R(x,z) `V  `!R(z,x), \quad  \emph{`!R(b,a)}\}
\end{eqnarraybleu}
avec \bleu{`s_3} la substitution identité,
\begin{eqnarraybleu}
  S_3 &=& \{`!R(x,x),\quad`!R(y,z) `V `!R(z,u) `V R(y,u),\quad
  R(a,b),\quad R(b,a),\\ % 
  && `!(a=b),\quad `!R(x,z) `V  `!R(z,x), \quad `!R(b,a), \quad `[] \}
\end{eqnarraybleu}
\end{footnotesize}
\end{slide}
%------------------------------------------------------
\begin{slide}
\begin{scriptsize}
  \begin{displaymathbleu}
    \hspace*{-20pt} \xymatrix @C 3pt {
      `!R(x,x) \ar@{-}[dr]&& `!R(y,z) `V `!R(z,u) `V R(y,u)\ar@{-}[dl]\\
      &`!R(x,z) `V  `!R(z,x) \ar@{-}[dr] && R(a,b)\ar@{-}[dl]\\
      &&`!R(b,a) \ar@{-}[dr] &&& R(b,a)\ar@{-}[dll]\\
      &&&`[]
    }
  \end{displaymathbleu}
\end{scriptsize}
\end{slide}
%------------------------------------------------------
\begin{slide}
On remarque que l'on n'a pas utilisé les propriétés de l'égalité. 

A la place de \bleu{a = b} on aurait pu mettre n'importe quelle propriété.
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Stratégies} %
%
La stratégie qui consiste à toujours choisir la dernière clause
produite s'appelle la \emph{résolution linéaire}.

La \verdir{stratégie linéaire} est \verdir{complète}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{Stratégie SLD}}}
\end{center}

    \begin{center}
      {\large \bf \color{vertfonce}{\textit{et}}}
    \end{center}

  \begin{center}
 {\large \bf \color{vertfonce}{\textit{programmation logique}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Clause de Horn} %
%
  Une clause qui contient \verdir{au plus un littéral positif} est
  appelée une \emph{clause de Horn}.

  Une clause qui contient \verdir{un et un seul littéral positif} est
  appelée une \emph{clause définie}.
  
  Au lieu de \bleu{`!A_1 `V \ldots `V `!A_n `V B} on écrit \bleu{B
    "<-" A_1, \ldots, A_n}.

  \vspace*{20pt}

  Une clause qui  contient \verdir{seulement des littéraux négatifs} est appelée un
  \emph{but}.

  Au lieu de \bleu{`!A_1 `V \ldots `V `!A_n} on écrit \bleu{"<-" A_1, \ldots, A_n}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La stratégie SLD} %
%
Soit \bleu{S} un ensemble de clauses de Horn composé d'un ensemble \bleu{D} de clauses définies, et d'un ensemble
\bleu{\{G_1,\ldots, G_q\}} de buts.

Une \emph{SLD-dérivation} est une suite de buts \bleu{\langle N_0, \ldots, N_p\rangle} tels que
\begin{itemize}
\item \bleu{N_0 = G_j} est l'un des buts,
\item si \bleu{N_i =\quad "<-" A_1, \ldots, A_{k-1}, A_{k},A_{k+1},\ldots, A_n}\ali et s'il y a une clause définie
  \bleu{A "<-" B_1, \ldots, B_m}, telle que \bleu{`s} est l'unificateur le plus général de \bleu{A_k} et \bleu{A}, %
  \ali  alors (cas \bleu{m>0}) \\
  \bleu{N_{i+1} =\quad "<-" `s(A_1, \ldots, A_{k-1}, B_1, \ldots, B_m,A_{k+1},\ldots, A_n)} \ali ou (cas \bleu{m=0})\\
  \bleu{N_{i+1} = \quad"<-" `s(A_1, \ldots, A_{k-1},A_{k+1},\ldots, A_n)}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La stratégie SLD} %
%
Une \emph{SLD-réfutation} est une \verdir{SLD-dérivation}  dans laquelle \bleu{N_p = `[]}.

La \emph{SLD-résolution} est la méthode qui consiste à montrer  qu'un ensemble de clauses de Horn est insatisfiable en
trouvant une \verdir{SLD-réfutation}. 

\vspace*{20pt}

\fbox{\parbox{7.5cm}{La SLD-résolution est complète pour les clauses de Horn.}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La programmation logique} %
%
La \emph{programmation logique} est une méthode qui consiste 
\begin{itemize}
\item à présenter des prédicats récursivement par un ensemble des
  clauses définies avec le même symbole relationnel en position de
  littéral positif,

\item à poser des questions par des buts.
\end{itemize}
Les clauses définies sans antécédents sont souvent vues comme l'énoncé de \emph{faits} (comme dans une base de données).
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La programmation logique} %
%
\textsc{Prolog} est donc un langage de programmation

où \emph{les procédures sont des clauses définies},

où \emph{l'appel se fait par unification}, c'est-à-dire que l'on effectue une unification (et pas seulement un filtrage
comme en CAML) entre le paramètre de la procédure appelée et la valeur fournie par l'appelant.

La question est plutôt une \emph{contrainte à résoudre}, que l'appelé identifie avec les contraintes qu'il sait
résoudre.  

\textsc{Prolog} fait donc partie des \emph{langages de résolution de contraintes}.

\textsc{Prolog} est lié aux \emph{langages d'interrogation de bases de données}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{brunfonce}{\textit{Un exemple : la théogonie d'Hésiode}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\slidepagestyle{empty}
  \begin{scriptsize}
    \begin{math}
\hspace*{-20pt}
      \begin{array}{l@{\hspace*{-10pt}}l}
      \begin{array}{ll}
 \mere{Mnémosyné}{Gaia} "<-" &   \pere{Mnémosyné}{Ouranos} "<-" \\
 \mere{Rhéa}{Gaia} "<-" &   \pere{Rhéa}{Ouranos} "<-" \\
 \mere{Cronos}{Gaia} "<-" &   \pere{Cronos}{Ouranos} "<-" \\
 \mere{Histié}{Rhéa} "<-" &   \pere{Histié}{Cronos} "<-" \\
 \mere{Déméter}{Rhéa} "<-" &   \pere{Déméter}{Cronos} "<-" \\
 \mere{Héra}{Rhéa} "<-" &   \pere{Héra}{Cronos} "<-" \\
 \mere{Zeus}{Rhéa} "<-" &   \pere{Zeus}{Cronos} "<-" \\
 \mere{Poséïdon}{Rhéa} "<-" &   \pere{Poséïdon}{Cronos} "<-" \\
 \mere{Hadès}{Rhéa} "<-" &   \pere{Hadès}{Cronos} "<-" \\
 \mere{Perséphone}{Déméter} "<-" &   \pere{Perséphone}{Zeus} "<-" \\
 \mere{Hébé}{Héra} "<-" &   \pere{Hébé}{Zeus} "<-" \\
 \mere{Arès}{Héra} "<-" &   \pere{Arès}{Zeus} "<-" \\
 \mere{Ilithye}{Héra} "<-" &   \pere{Ilithye}{Zeus} "<-" \\
 \mere{Clio}{Mnémosyné} "<-" &   \pere{Clio}{Zeus} "<-" \\
 \mere{Calliope}{Mnémosyné} "<-" &   \pere{Calliope}{Zeus} "<-"
      \end{array}
&
\begin{array}{l}
\textrm{grand-père(\brunir{x}, \brunir{y})} "<-" \pere{x}{z}, \pere{z}{y}\\
\textrm{grand-père(\brunir{x}, \brunir{y})} "<-" \mere{x}{z}, \pere{z}{y}\\\\
\textrm{grand-mère(\brunir{x}, \brunir{y})} "<-" \pere{x}{z}, \mere{z}{y}\\
\textrm{grand-mère(\brunir{x}, \brunir{y})} "<-" \mere{x}{z},\mere{z}{y}\\\\
\textrm{cousin(\brunir{x},\brunir{y})} "<-" \textrm{grand-père(\brunir{x},\brunir{z})},\textrm{grand-père(\brunir{y},\brunir{z})}   \\
\textrm{cousin(\brunir{x},\brunir{y})} "<-"
    \textrm{grand-mère(\brunir{x},\brunir{z})},\textrm{grand-mère(\brunir{y},\brunir{z})}\\\\
\textrm{ancêtre(\brunir{x},\brunir{y})} "<-" \pere{x}{y}\\
\textrm{ancêtre(\brunir{x},\brunir{y})} "<-" \mere{x}{y}\\
\textrm{ancêtre(\brunir{x},\brunir{y})} "<-" \pere{x}{z}, \textrm{ancêtre(\brunir{z},\brunir{y})}\\
\textrm{ancêtre(\brunir{x},\brunir{y})} "<-" \mere{x}{z}, \textrm{ancêtre(\brunir{z},\brunir{y})}
\end{array}
    \end{array}
    \end{math}
  \end{scriptsize}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Quelques questions} %
%
\emph{Simple à solution unique}\\
\begin{math}
  "<-" \mere{Clio}{x}\\
  "<-" \mere{Persphone}{x}, \pere{x}{y}, \textrm{reponse}(\brunir{x})
\end{math}

\vspace*{5pt}

\emph{Simple à solutions multiples}\\
\begin{math}
    "<-" \pere{x}{Zeus}\\
  "<-" \textrm{grand-père(\brunir{Perséphone}, \brunir{x})}\\
    "<-" \textrm{grand-père(\brunir{x}, \brunir{Zeus})}\\
    "<-" \textrm{grand-père(\brunir{x}, \brunir{y})}
\end{math}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Quelques questions} %
%
\emph{Solutions d'une relation} (question non linéaire)\\
  \begin{math}
    "<-" \textrm{cousin(\brunir{x},\brunir{y})}, \pere{x}{y}\\ % réponse: Zeus et Clio
    "<-" \textrm{oncle(\brunir{x},\brunir{x})} \textrm{\quad si on a
      déjà défini oncle.}
    \\\\
    \hspace*{20pt} \textrm{oncle(\brunir{x},\brunir{y})} "<-" \textrm{grand-père(\brunir{x},\brunir{z})},\pere{y}{z}\\
     \hspace*{20pt} \textrm{oncle(\brunir{x},\brunir{y})} "<-"
    \textrm{grand-mère(\brunir{x},\brunir{z})},\mere{y}{z}
  \end{math}
\vfill
\end{slide}
\end{document}
% LocalWords:  clausales clausale séquent sous-preuve vertfonce skolémisée cut
% LocalWords:  résolvants width attention.eps ud uds l'analogie skolémiser FV
% LocalWords:  irréflexive mgu brunfonce Horn Insatisfiabilité SLD théogonie
% LocalWords:  SLD-dérivation SLD-réfutation SLD-résolution d'Hésiode Clio
