%% Time-stamp: <modified on 29 Nov 2004 at 15:27 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[latin1]{inputenc}
\usepackage{color}
%\usepackage{amsmath}
\usepackage[all]{xy}
\input{mes_couleurs}
\usepackage{qsymbols}
\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{Complétion}

\date{}

\pagestyle{}

\slidestyle{empty}

\slideframe{}   

%--- couleurs ----
\renewcommand{\emph}[1]{\rouge{#1}}

%--- symboles ---
\renewcommand{\phi}{\varphi}
%\newcommand{\llbracket}{\ensuremath{|\![}}
%\newcommand{\rrbracket}{\ensuremath{]\!|}}
\newcommand{\Emb}{\bl{\ensuremath{\cal EMB}}}
\newcommand{\ali}{\newline\hspace*{20pt}}
\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{\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{?}{=}}

%%%%%%%%% ajout special pour la completion %%%%%%%%%%%%
\newcommand{\la}{\leftarrow}
%\newcommand{\rastar}{\stackrel{\ast}{\rightarrow}}
\newcommand{\hligne}{\rule{\textwidth}{2pt}}
%\newcommand{\subsum}{\mbox{\small \tt |}\hspace{-2.9pt}{\stackrel{\scriptscriptstyle _\bullet}{}\hspace{-5pt}>}}
\newcommand{\subsum}{\mathop{\raisebox{1pt}{$\scriptscriptstyle \bullet$}\hspace{-7pt}\vartriangleright}}
\newcommand{\eqone}{\mbox{\mysymb \symbol{1}}}
\newcommand{\tri}{\mbox{\mysymb \symbol{2}}}
%%%%%%%% fin ajout %%%%%%%%%

\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{bdp}[1]{\begin{displaymath}\color{blue}#1}{\end{displaymath}}
    
%% ==============================================================
%%                   Reductions and other relations
%% ==============================================================

%\newcommand{\ra}{\xymatrix{\ar@{>}[r] &}}
\newcommand{\ra}{\rightarrow}
\newcommand{\ranorm}{\xymatrix{\ar@{>>|}[r] &}}
\newcommand{\rara}{\xymatrix{\ar@{>>}[r] &}}
\newcommand{\longequiv}{\xymatrix{\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{\ar@{>}[r]_{#1} &}}
\newcommand{\subar}[1]{\xymatrix{\ar@{<-}[r]_{#1} &}}
\newcommand{\ranormsub}[1]{\xymatrix{\ar@{>>|}[r]_{#1} &}}
\newcommand{\rarasub}[1]{\xymatrix{\ar@{>>}[r]_{#1} &}}
\newcommand{\rasup}[1]{\xymatrix{\ar@{>}[r]^{#1} &}}
\newcommand{\supar}[1]{\xymatrix{\ar@{<-}[r]^{#1} &}}
\newcommand{\rarasup}[1]{\xymatrix{\ar@{>>}[r]^{#1} &}}
\newcommand{\rasupsub}[2]{\xymatrix{\ar@{>}[r]^{#1}_{#2} &}}
\newcommand{\rarasupsub}[2]{\xymatrix{\ar@{>>}[r]^{#1}_{#2} &}}
\newcommand{\cv}[1]{\xymatrix{\ar@{<->}[r]_{#1} &}}
\newcommand{\conv}[1]{\xymatrix{\ar@{<->}[r]_{#1}^{*} &}}
\newcommand{\convplus}[1]{\xymatrix{\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}^{*} &}}

\newenvironment{displaymathbleu}%
  {\begin{displaymath}\color{blue}}
  {\end{displaymath}}

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

%%%%%%%%%%%%%%%%% Headings %%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\heading}[1]{%
{\color{vertfonce}\bf\large #1}{\color{yellow}\\\rule{\textwidth}{2pt}}
}
\newcommand{\subheading}[1]{%
  \begin{center}
    \color{green}{\bf\Ovalbox{#1}}
  \end{center}}

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

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

\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{brunfonce}{\textit{Le lemme de Knuth-Bendix et la
          confluence locale}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Paires critiques}
%
Si il existe \begin{itemize}
\item deux
règles \bleu{l\ra r} et \bleu{g\ra d} %
\ali {\footnotesize dont on suppose les ensembles de variables
  disjoints},

\item une position \bleu{p\in Pos(l)}, qui n'est pas la position d'une
variable,  

\item un mgu  \bleu{\sigma} de \bleu{l_{|p}} et de \bleu{g}.

\end{itemize}

Le terme \bleu{\sigma(l)} est appelé une  \emph{superposition}

et la paire \bleu{\langle\sigma(r)~ ,~ \sigma(l[d]_p)\rangle}
est appelée 
\emph{une paire critique.}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Paires critiques}
%
Si il existe \begin{itemize}
\item deux règles \bleu{l\ra r} et \bleu{g\ra d} %
  \ali {\footnotesize dont on suppose les ensembles de variables
    disjoints},

\item une position \bleu{p\in Pos(l)}, qui n'est pas la position d'une
variable,  

\item un mgu  \bleu{\sigma} de \bleu{l_{|p}} et de \bleu{g}.

\end{itemize}

Le terme \bleu{\sigma(l)} est appelé une  \emph{superposition}

et la paire \bleu{\langle\sigma(r)~ ,~ \sigma(l[d]_p)\rangle}
est appelée 
\emph{une paire critique.}
\vfill
\verdir{Le problème est de savoir si les paires critiques sont
\emph{joignables}.}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les positions non prises en compte}
%
\verdir{Position non variable}

Si dans la définition, on acceptait une position \bleu{p\in Pos(l)} qui
est la position d'une variable \bleu{x}, alors
\begin{itemize}
\item il y aurait toujours un mgu de  \bleu{\sigma} de \bleu{l_{|p}} et de
  \bleu{g}, à savoir \bleu{\{x"|->"g\}},
\item il y aurait donc toujours une paire issue de cette superposition
  (triviale), à savoir
  \bleu{\langle\{x"|->"g\}(r)~ ,~ \langle\{x"|->"g\}\l[d]_p\rangle},
  
\item cette paire critique serait joignable vers le terme
  \bleu{\{x"|->"d\}(r)}.
\end{itemize}
\vfill \textbf{Donc on ne considère pas les positions dans \bleu{l}
  qui correspondent à des variables.}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les positions non prises en compte}
%
\verdir{Superposition à la racine dans le cas où} \bleu{l\ra r `= g\ra
  d}.

Dans ce cas, la superposition est triviale, le mgu est la substitution
identité et la paire critique est évidemment joignable.

\textbf{On ne considère donc pas les superpositions à la racine d'une règle
sur elle-même.}

\emph{En revanche}, d'autres superpositions peuvent exister comme dans le
cas où 
\begin{itemize}
\item \bleu{l\ra r `= (x_1 * y_1) * z_1 \ra x_1 * (y_1 *z_1)} 
\item et
  \bleu{g\ra d `= (x_2 * y_2) * z_2 \ra x_2 * (y_2 *z_2)}.
\end{itemize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{brunfonce}{\textit{Un exemple}}}
\end{center}
\end{slide}
%----------------------------------------------------------------------------
%                              ASSOC + ENDO
%----------------------------------------------------------------------------
\begin{slide}{}
\heading{associativit\'e + endomorphisme}

\begin{eqnarray}
(x * y) * z & \ra & x * (y * z) \\
f(x) * f(y) &\ra & f(x * y)
\end{eqnarray}
\vfill
\end{slide}

%---------------------------------------------------------------------

\begin{slide}{}
\heading{Paires Critiques}
\begin{eqnarray*}
(f(x) * f(y)) * z & \stackrel{1}{\ra} & f(x) * (f(y) * z)
\\
\\
&  \stackrel{2}{\ra} & f(x * y) * z
\end{eqnarray*}

$(f(x) * f(y)) * z $ est une \rouge{superposition} \ali de la règle (1)
dans la règle (2).

\begin{displaymathbleu}
  \langle f(x) * (f(y) * z), f(x * y) * z\rangle
\end{displaymathbleu}
est une  \rouge{paire critique} \emph{\textbf{non joignable}}.

\end{slide}
%------------------------------------------------------
\begin{slide}

$((x_1 * x_2) *y) * z $ est une \rouge{superposition} \ali de la règle (2)
dans la règle (2).

\begin{eqnarray*}
  ((x_1 * x_2) *y) * z &  \stackrel{2}{\ra} & (x_1 * (x_2 * y)) * z\\
&  \stackrel{2}{\ra} & (x_1 * x_2) * (y * z)
\end{eqnarray*}

\begin{displaymathbleu}
  \langle (x_1 * (x_2 * y)) * z, (x_1 * x_2) * (y * z) \rangle
\end{displaymathbleu}
est une  \rouge{paire critique} \emph{\textbf{joignable}}, puisque les deux
membres se r\'e\'ecrivent vers le m\^eme terme.

\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Théorème de Knuth et Bendix} 
  
  \framebox{\parbox{8.5cm}{Etant donné un système de réécriture
      \bleu{R}.  \ali \bleu{R} est localement confluent si et
      seulement si toutes ses paires critiques sont joignables.}}

La condition est clairement nécessaire.


\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
Pour la condition suffisante, il faut examiner les triplets

\begin{center}
\bl{
\xymatrix{
&t \ar[ld]_p \ar[rd]^q &\\
u && v
}}
\end{center}

et considérer les positions respectives de \bleu{p} et \bleu{q} et les
régles \bleu{l\ra r} et \bleu{g\ra d} qui permettent de réécrire
\bleu{t}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\parbox{4cm}{Si \bleu{p} et \bleu{q} sont étrangers alors
\begin{itemize}
\item \bleu{u\rasupsub{q}{g\ra d, \rho} u'} 
\item \bleu{v\rasupsub{p}{l\ra r,\theta} v'}, 
\item et \bleu{u'\equiv v'}.
\end{itemize}}
\hfill    \includegraphics[width=4.2cm]{1.eps}
\end{slide}
%------------------------------------------------------
\begin{slide}
Si \bleu{p} est un préfixe de \bleu{q} (avec \bleu{q\equiv p
q'}) et \bleu{q'\in Pos(l)}, alors \begin{itemize}
\item \bleu{t_{|p} = \theta(l)} est
l'instance d'une superposition,
\item et \bleu{\langle \theta(r)~,~ \theta(l[d]_{q'}\rangle}, est
l'instance d'une paire critique entre \bleu{l\ra r} et \bleu{g\ra d},
\item on a le résultat parce que la paire critique
est joignable.
\end{itemize}
   \centerline{\includegraphics[width=5cm]{2.eps}}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{tabular}{lr}
\parbox{4.5cm}{Si \bleu{p} est un préfixe de \bleu{q} (avec \bleu{q\equiv p
q'}) et \bleu{q'\notin Pos(l)}, on peut réécrire les ``résidus''.}
&
   \includegraphics[width=3.9cm]{3.eps}
  \end{tabular}
\end{slide}
%-----------------------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{brunfonce}{\textit{La compétion en Orme}}}
\end{center}

\end{slide}
% ----------------------------------------------------------------------

\begin{slide}{}

\heading{Proc\'edure de Compl\'etion}

Une \emph{proc\'edure de compl\'etion\/} transforme un ensemble de
d'identit\'{e}s en un ensemble \'{e}quivalent de r\`{e}gles confluentes et qui
se terminent.

Plus g\'{e}n\'{e}ralement, une proc\'edure de compl\'etion transforme
\begin{itemize}
\item un ensemble d'identit\'{e}s et de r\`{e}gles qui se terminent
\item en un ensemble \'{e}quivalent de r\`{e}gles confluentes et qui
  se terminent.
\end{itemize}

Cela n\'{e}cessite un ordre pour orienter les identit\'{e}s.
\vfill
\end{slide}

% ----------------------------------------------------------------------
%               EXEMPLE de COMPLETION
%------------------------------------------------------
\begin{slide}{}
\heading{Les composants d'ORME}
Les composants en \emph{rouge} sont des conteneurs qui ne contiennent
qu'une règle, les autres sont des listes d'objets.

Les extensions\textbf{ X\_ext} ne sont pas utilisés.
\vfill
\end{slide}
%-----------------------------------------------------------------------
\begin{slide}{}
\heading{Les composants d'ORME}
\begin{small}
\begin{description}
\item[AC\_op] les opérateurs associatifs et commutatifs,
\item[C\_op] les opérateurs commutatifs,
\item[E\_raw] les identités telles quelles,
\item[E\_norm] les identités après normalisation par les règles du
  système,
\item[\emph{S}] une règle qui vient d'être orientée sert à simplifier,
\item[T] les règles en attente de traitement,
\item[\emph{C}] la règle dont on calcule toutes les paires critiques,
\item[N] les règles dont la paire critique avec \emph{C} n'a pas
  encore été calculée.
\item[A] les règles dont la paire critique avec \emph{C} a déjà été
  calculée,
\end{description}
\end{small}
\vfill
\end{slide}
%-----------------------------------------------------------------------
\begin{slide}{}
\heading{Quelques étapes d'ORME}
\begin{description}
\item[New loop] démarrage d'une nouvelle boucle de calcul de paires
  critiques,


\item[ Cleaning of E\_raw]  nettoyage de \textbf{E\_raw} pour créer
  \textbf{E\_nor}, 
\item[Orientation of E\_nor] orientation d'une égalité normalisée,

\item[Simplification] utilisation de \emph{\textbf{S}} pour simplifier
  les autres composants,
\item[C\_internal\_Deduction] calcul des paires critiques de
  \emph{\textbf{C}} sur elle-même,
\item[N\_C\_Deduction] calcul des paires critiques de
  \emph{\textbf{C}} avec celle de \emph{N}.
\end{description}
\vfill
\end{slide}
%-----------------------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{brunfonce}{\textit{Un exemple de
          compl\'{e}tion}}}
\end{center}

\begin{center}
  {\large \bf \color{brunfonce}{\textit{La présentation des groupes de
        Taussky}}}
\end{center}
\end{slide}
%-----------------------------------------------------------------------
\begin{slide}{}
\heading{L'exemple de Taussky}
\brunir{\bleu{*} est associatif}
\begin{eqnarraybleu}
  x * (y * z) &=& (x * y) * z \qquad \qquad \emph{(A)}
\end{eqnarraybleu}
\brunir{Il existe un élément idempotent:}
\begin{eqnarraybleu}
  e * e &=& e \qquad \qquad \emph{(Id)}
\end{eqnarraybleu}
\brunir{Chaque élément a au moins un inverse à droit vis-à-vis de \bleu{e}:}
\bleu{(`A x) (`E y)\ x * y = e,}
ce qui donne par skolémisation:
\begin{eqnarraybleu}
  x * i(x) &=& e \qquad \qquad \emph{(InvD)}
\end{eqnarraybleu}
\vfill
\end{slide}
%-----------------------------------------------------------------------
\begin{slide}{}
\heading{L'exemple de Taussky}
\brunir{Chaque élément a au plus un inverse à gauche vis-à-vis de \bleu{e}: }
\begin{displaymathbleu}
  (`A x)\ (`A x')\ (`A y)\quad x * y = x' * y = e \quad "=>" \quad x =
  x' \qquad \qquad \emph{(InvG)}
\end{displaymathbleu}
ce qui est équivalent aux deux équations \textit{\emph{(T)}}:
\begin{eqnarraybleu}
  g(x * y, y) &=& f(x * y,x)\\
  f(e,x) &=& x.
\end{eqnarraybleu}
\vfill
\end{slide}
%-----------------------------------------------------------------------
\begin{slide}{}
\heading{L'exemple de Taussky}
\framebox{\parbox{2cm}{\textit{\emph{(T)}} $"=>"$\textit{\emph{(InvG)}}}}

Supposons \bleu{z'* z = z'' * z = e}.
\begin{eqnarraybleu}
  z' & = & f(e, z') = f(z' * z, z') = g(z' * z, z) \\
  &=& g(z'' * z, z) = f(z''*z,z'') = f(e, z'')\\
  &=& z''.
\end{eqnarraybleu}

\vfill
\end{slide}
%-----------------------------------------------------------------------
\begin{slide}{}
\heading{L'exemple de Taussky}
\framebox{\parbox{4.3cm}{\textit{\emph{(A)} + \emph{(Id)} + \emph{(InvD)} +
\emph{(InvG)}}  $"=>"$ \textit{\emph{(T)}}}}

On montre que l'ajout de \emph{(T)} est \emph{conservatif} autrement
  dit, si \bleu{s,t\in T(\{*, i, e),X)\}} alors

      \begin{center}
        $ \emph{(A)} + \emph{(Id)} + \emph{(InvD)} + \emph{(InvG)} +
        \emph{(T)} "|-" s = t $
      \end{center}
    
    \begin{center}
      $\emph{"=>"}$
    \end{center}
  
    \begin{center}
      $\emph{(A)} + \emph{(Id)} + \emph{(InvD)} + \emph{(InvG)} "|-" s
      = t$
    \end{center}
  \vfill
\end{slide}
%-----------------------------------------------------------------------
\begin{slide}{}
  En effet, \textit{\emph{(T)}} n'ajoute pas de nouvelles
  équations entre termes de \bleu{T(\{*, i, e),X)\}}, car une telle chaîne
  passerait par \bleu{s = f(e,s')= \ldots = g(e, u) `= g(s' * u, u) = g(t' *
  u, u) = \ldots = f(e, t') = f(e,t)}.  Ce qui implique que \bleu{s = s' =
  t' = t} puisque \bleu{u} a au plus un inverse à gauche vis-à-vis de \bleu{e}.
\vfill
\end{slide}
%-----------------------------------------------------------------------
\begin{slide}{}
\heading{L'exemple de Taussky}
On obtient les dix axiomes classiques plus les deux règles:
\begin{eqnarraybleu}
  f(e,x) &"->"& x\\
g(x,y) &"->"& f(x, x* i(y)).
\end{eqnarraybleu}
\vfill
\end{slide}
%-----------------------------------------------------------------------
\begin{slide}{}
\rouge{Groupes (Axiomes de Taussky)}
\begin{eqnarray*}
(x * y) * z & \ = \ & x * (y * z)\\
e * e  & \ = \ & e\\
x * i(x)  & \ = \ & e\\
g(x * y, y)  & \ = \ & f(x * y, x) \\
f(e,x)  & \ = \ & x
\end{eqnarray*}
\end{slide}
%-----------------------------------------------------------------------
\begin{slide}
\rouge{Groupes (Axiomes de Taussky, système complété)}
\begin{scriptsize}

  \begin{math}
    \begin{array}{rcl}
    (x * y) * z & \ \ra \ & x * (y * z)\\
    e * x & \ \ra \ & x\\
    x * e & \ \ra \ & x\\
    i(x) * x & \ \ra \ & e\\
    x * i(x) & \ \ra \ & e\\
    i(i(x)) & \ \ra \ & x\\
    i(e)  & \ \ra \ & e \\
    i(x * y)  & \ \ra \ & i(y) * i(x)\\
    x * (i(x) * y) & \ \ra \ & y \\
    i(x) * (x * y) & \ \ra \ & y\\
    \multicolumn{3}{c}{\rule{130pt}{1pt}}\\
    g(x,y)  & \ \ra \ & f(x,  i(y) * x)\\
    f(e,x) & \ \ra \ & x
  \end{array}
\end{math}
\end{scriptsize}
\end{slide}
% ----------------------------------------------------------------------
%               LA PROC\'{E}DURE DE COMPLETION
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{brunfonce}{\textit{La proc\'{e}dure de compl\'{e}tion}}}
\end{center}
\end{slide}
%-----------------------------------------------------------------------
\begin{slide}{}
\heading{L'enchâssement}
La relation d'enchâssement \emph{$\subsum$} (en anglais encompassment)
est définie par 
\bl{
\[s \subsum t \]
}
\centerline{si et seulement si}
\bl{
\[s \not= t \quad \textrm{et} \quad \exists p \in Pos(s) \cdot \exists
\sigma\in Sub(T(\Sigma, V)) \cdot \quad s_{|p} = \sigma(t) \]
}
\vfill
\bleu{\subsum} termine.
\end{slide}
%-----------------------------------------------------------------------
\begin{slide}{}
\begin{footnotesize}
\begin{displaymath}
\begin{array}{lrcll}
\mbox{\emph{Delete:}} & E \cup \{s=s\};R & \;\vdash\; & E;R \\ \\
\mbox{\emph{Compose:}} & E;R \cup \{s \ra t\} & \;\vdash\; & E;R \cup \{s \ra u\}
        \\
        & \lefteqn{\mbox{\verdir{si~}} t \raR u}\\ \\
\mbox{\emph{Simplify:}} & E \cup \{s=t\};R & \;\vdash\; & E \cup \{s=u\};R
        \\
         & \lefteqn{\mbox{\verdir{si~}} t \raR u}
\end{array}
\end{displaymath}
\end{footnotesize}
\end{slide}

%-----------------------------------------------------------------------
\begin{slide}{}
\begin{footnotesize}
\begin{displaymath}
\begin{array}{lrcll}
\mbox{\emph{Collapse:}} & E;R \cup \{s \ra t\} & \;\vdash\; & E \cup \{u=t\};R 
        \\
        & \lefteqn{\mbox{\verdir{si~}} s \raR u}\\
 & \lefteqn{\mbox{\verdir{par une r\`{e}gle\ }} l \ra r \in R} \\
 & \lefteqn{\mbox{\verdir{avec\ }} s \subsum l} \\
 & \lefteqn{\mbox{\verdir{\ \ \ ou\ }} s=l \mbox{\verdir{\ et \ }} t > r}\\[2pt]
\mbox{\emph{Orient:}} & E \cup \{s=t\};R & \;\vdash\; & E;R \cup \{s \ra t\}
        \\
        & \lefteqn{\mbox{\verdir{si~}} s > t }\\[2pt]
\mbox{\emph{Deduce:}} & E;R & \;\vdash\; & E \cup \{s=t\};R
        \\
        & \lefteqn{\mbox{\verdir{si~}} s \subar{R} u  \raR t} \\
 & \lefteqn{\mbox{\verdir{\ pour un\ }} u}
\end{array}
\end{displaymath}
\end{footnotesize}
\end{slide}

% ------------------------------------------------------------------------
%                     COMPLéTION de ASSOC + ENDO
% ------------------------------------------------------------------------
\begin{slide}{}
\heading{Completion de l'{\it associativit\'e + endomorphisme}}

Commen\c{c}ons par 
\[E_0 \equiv \{e_1,e_2\}\] et
\[R_0 \equiv \emptyset,\] o\`u

\[\begin{array}{rcrl}
e_1 & \equiv & (x * y) * z &  =  x * (y * z) \\
e_2 & \equiv & f(x) * f(y) & = f(x * y)
\end{array} \]

\end{slide}

% ----------------------------------------------------------------------
\begin{slide}{}
\begin{center}
\begin{tabular}{|c|}\hline
\(e_1,e_2\)\\
\hline
\ \\
\hline
\end{tabular}

\(\stackrel{\mbox{\small \it Orient}}{\vdash}\)

\begin{tabular}{|c|}\hline
\(e_2\)\\
\hline
\((x * y) * z \ra  x * (y * z) \)\\
\hline
\end{tabular}

\(\stackrel{\mbox{\small \it Deduce}}{\vdash}\)

\begin{tabular}{|c|}\hline
\(e_2,(x_1 * (x_2 * y)) * z = (x_1 * x_2) * (y *z)\) \\
\hline
\(r_1\) \\
\hline
\end{tabular}

\(\stackrel{\mbox{\small \it Simplify}}{\vdash}\)

\begin{tabular}{|c|}\hline
\(e_2, x_1 * ((x_2 * y) * z) = (x_1 * x_2) * (y *z)\)\\
\hline
\(r_1\)\\
\hline
\end{tabular}
\end{center}
\end{slide}

% -------------------------------------------------------------------------

\begin{slide}{}
\begin{center}

\(\vdots\)

\(\stackrel{\mbox{\small \it Simplify}}{\vdash}\)

\begin{tabular}{|c|}\hline
\(e_2, x_1 * (x_2 * (y * z)) = x_1 * (x_2 * (y *z))\)\\
\hline
\(r_1\)\\
\hline
\end{tabular}

\(\stackrel{\mbox{\small \it Delete}}{\vdash}\)

\begin{tabular}{|c|}\hline
\(e_2\)\\
\hline
\(r_1\)\\
\hline
\end{tabular}

\end{center}

\end{slide}

% -------------------------------------------------------------------------

\begin{slide}{}
\begin{center}

\(\stackrel{\mbox{\small \it Orient}}{\vdash} \)

\begin{tabular}{|c|}\hline
\( \) \\
\hline
\(r_1,f(x) * f(y) \ra f(x * y)\)\\
\hline
\end{tabular}

\(\stackrel{\mbox{\small \it Deduce}}{\vdash}\)

\begin{tabular}{|c|}\hline
\(f(x) * (f(y) * z) = f(x * y) * z \) \\
\hline
\(r_1,r_2\)\\
\hline
\end{tabular}

\(\stackrel{\mbox{\small \it Orient}}{\vdash}\)

\begin{tabular}{|c|}\hline
\( \)\\
\hline
\(r_1,r_2, f(x) * (f(y) * z) \ra f(x * y) * z\)\\
\hline
\end{tabular}

\(\stackrel{\mbox{\small \it Deduce}}{\vdash}\)

\begin{tabular}{|c|}\hline
\( f(x) * f(y * z) = (f(x) * f(y)) * f(z)\)\\
\hline
\(r_1,r_2,r_3\)\\
\hline
\end{tabular}
\end{center}


\end{slide}

% ----------------------------------------------------------------------

\begin{slide}{}
\begin{center}
\(\vdots\)

\(\stackrel{\mbox{\small \it Delete}}{\vdash}\)

\begin{tabular}{|c|}\hline
\( \)\\
\hline
\((x * y) * z \ra  x * (y * z)\) \\
\(f(x) * f(y) \ra f(x * y)\)\\
\(f(x) * (f(y) * z) \ra f(x * y) * z\)\\
\hline
\end{tabular}
\end{center}

\end{slide}


% --------------------------------------------------------------------------
%               Qu'EST-CE QUE LA COMPLéTION ?
% --------------------------------------------------------------------------

\begin{slide}{}
\heading{\large Qu'est-ce que la COMPL\'{E}TION ?}

\begin{footnotesize}
\begin{description}
\item[des r\`egles de transitions]: 
        \begin{scriptsize}
        \begin{itemize}
        \item{\it Orient\/}, 
        \item{\it Simplify\/},...
        \end{itemize}
        \end{scriptsize}
                
\item[un contr\^ole \'equitable]
\item[une bo\^{\i}te \`a outils] avec   
        \begin{scriptsize}
        \begin{itemize}
        \item l'unification, 
        \item le filtrage, 
        \item la r\'e\'ecriture,...
        \end{itemize}
        \end{scriptsize}
\end{description}
{\center +}
\begin{description}
\item[une structure de donne\'es] ici $(R,E)$ \qquad ou \qquad (E\_raw,
  E\_norm, \emph{S}, T, \emph{C}, N, A).
\end{description}
\end{footnotesize}
\end{slide}


% --------------------------------------------------------------------------
%                       Les ensembles Rj et Ej
% --------------------------------------------------------------------------

\begin{slide}{}
\heading{Les ensembles \bleu{R_j} et \bleu{E_j}}
Une complétion peut-\^{e}tre \emph{infinie}.

Au cours de son déroulement, la complétion peut créer une infinité
d'ensembles \bleu{R_j} et \bleu{E_j}.

On souhaite
\begin{itemize}
\item qu'une règle reste indéfiniment dans les \bleu{R_j} seulement si
elle ``doit'' y rester.

\item qu'une identité ne reste pas indéfiniment  dans les \bleu{E_j}.

\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------------------------
\begin{slide}{}
\heading{Les ensembles \bleu{R_j} et \bleu{E_j}}
Une complétion peut-\^{e}tre \emph{infinie}.

Au cours de son déroulement, la complétion peut créer une infinité
d'ensembles \bleu{R_j} et \bleu{E_j}.

On souhaite
\begin{itemize}
\item qu'une règle reste indéfiniment dans les \bleu{R_j} seulement si
elle ``doit'' y rester.

\item qu'une identité ne reste pas indéfiniment  dans les \bleu{E_j}.

\end{itemize}

\verdir{Cela a une conséquence sur le comportement  de la complétion, meme si
elle finit.}
\vfill
\end{slide}


% --------------------------------------------------------------------------
%                       EQUITE
% --------------------------------------------------------------------------

\begin{slide}{}
\begin{center}
\heading{Règles persistantes}
\end{center}

Une r\`egle \bleu{r} est \rouge{persistante} si elle appartient
ind\'efiniment aux \bleu{R_j} apr\`es avoir \'et\'e cr\'e\'ee,
\mbox{c-\`a-d} qu'il existe \bleu{i} tel que \bl{\[r\in \bigcap_{j\ge i}
R_j.\]}

\hligne 

L'\rouge{ensemble de r\`egles limite} ou ensemble de \rouge{r\`egles
persistantes} est \bl{\[R_{\omega} = \bigcup_{i\ge 0}\bigcap_{j\ge
  i}R_j\]} 
\end{slide}


% --------------------------------------------------------------------------

\begin{slide}{}
\heading{Identités persistantes}

Une \rouge{identit\'e} \bleu{e} est \rouge{persistante} si \bleu{e}
appartient ind\'efiniment \`a l'ensemble \bleu{E_j} une fois qu'elle a
été introduite, \mbox{c-\`a-d} qu'il existe un \bleu{j} tel que \bleu{e\in
\bigcap_{j\ge i} E_j}.

\hligne
\bl{\[E_{\omega} = \bigcup_{i\ge 0}\bigcap_{j\ge i}E_j\]} est l'ensemble des
identit\'es persistantes.
\vfill
\end{slide}
% --------------------------------------------------------------------------
\begin{slide}{}
  \heading{Paires crititiques persistantes}
  
  Une \rouge{paire critique} \bleu{pc} est \rouge{persistante}\ali si
  \bleu{pc} est une paire critique de \bleu{R_{\omega}}.
\hligne
\bl{\[PC_\omega = pc(R_\omega)\]}
\vfill
\end{slide}
% --------------------------------------------------------------------------
\begin{slide}{}
\begin{center}
\heading{Preuve par réécriture}
Une preuve par réécriture est une preuve de la forme:

\vspace*{15pt}

\bl{
\xymatrix{
s\ar[rd]_{*} && t\ar[ld]^{*}\\
& . &
}}
\end{center}
\vfill
\end{slide}
%----------------------------------------------------------------------

\begin{slide}{}
\heading{\'{E}quit\'e du contr\^ole}
%
Soit \bleu{R_E} le syst\`{e}me de r\'{e}\'{e}criture \emph{canonique}, (c-\`a-d
confluent, noeth\'erien et interr\'eduit)  associ\'{e} \`{a} \bleu{E} et
\bleu{>}.

S'il existe, \bleu{R_E} est \emph{unique\/}.

La compl\'{e}tion est \emph{\'{e}quitable} si pour toute preuve par
r\'{e}\'{e}criture dans \bleu{R_E}, il existe un \bleu{i} tel que
cette preuve est une preuve dans~\bleu{R_i}.

Autrement dit, le contr\^{o}le est \verdir{\'{e}quitable} si et seulement si

\bl{\[R_E = R_{\omega}\]}

\end{slide}


% --------------------------------------------------------------------------
\begin{slide}{}

\noindent \heading{Une condition suffisante d'\'{e}quit\'{e}}

Un contr\^ole est \'equitable si
\begin{itemize}

    \item Il n'existe pas d'identit\'es persistantes,

    \item Chaque paire critique persistante est t\^{o}t ou tard prise en consid\'{e}ration,

    \item Chaque r\`{e}gle persistante est r\'{e}duite.

\end{itemize}
\vfill
\end{slide}
% --------------------------------------------------------------------------
\begin{slide}{}
en d'autres termes

\vspace*{15pt}

%\begin{large}
\begin{center}
\begin{tabular}{||rl||}\hline\hline
$E_{\omega}$ & $=$ \quad $\emptyset$ \\ &\\
$pc(R_{\omega})$ & $\subseteq$  \quad ${\bigcup}_{i\ge 0} E_i$\\ & \\
$R_{\omega}$ & est r\'{e}duit  \\ \hline\hline
\end{tabular}
\end{center}
%\end{large}
                             \end{slide}

%---------------------------------------------------------------------
%                     Un contrexemple
%---------------------------------------------------------------------

\begin{slide}{}
\heading{Un contrexemple}
\bl{
\begin{eqnarray*}
f(g(h(x))) & \ra & g(x) \\
g(h(g(x))) & \ra & g(g(h(x)))\\
f(g(g(x))) & \ra & f(g(x)))
\end{eqnarray*}}
Si l'on l'on ne prend jamais en compte la troisième règle, \ali on
obtient les règles \bleu{f(g^{n+1}(h(x))) \ra g^{n+1}(x)}  
\vfill
\end{slide}

\begin{slide}{}
\begin{small}
Sinon on obtient le système:
\bl{
\begin{eqnarray*}
f(g(h(x))) & \ra & g(x) \\
g(h(g(x))) & \ra & h(x)\\
g(g(x)) & \ra & g(x)
\end{eqnarray*}}
puis
\bl{
\begin{eqnarray*}
f(h(x)) & \ra & g(x) \\
h(g(x)) & \ra & h(x)\\
g(h(x)) & \ra & h(x)\\
g(g(x)) & \ra & g(x)\\
f(g(x)) & \ra & g(x)
\end{eqnarray*}}
\end{small}
\end{slide}
%---------------------------------------------------------------------
%                      La philopsophie ORME                         #7
%---------------------------------------------------------------------

\begin{slide}{}
\heading{La construction d'une bonne complétion}
\begin{itemize}

\item Puisque les r\`egles de transition sont des bons outils de
preuves, pourquoi ne seraient-elles pas de bons outils d'implantation\,?

\item Une bonne \emph{structure de donn\'ees\/} est cruciale

\item La compl\'etion est comme une \emph{machine\/} avec la structure
de donn\'ees comme \'etats et les r\`egles de transition comme transitions.

\item Le contr\^{o}le ou la \emph{strat\'egie\/} nous dit comment
invoquer les r\`egles,

\item La \emph{bo{\^\i}te \`a outils\/} contient les composants de la
proc\'edure, ils peuvent \^etre r\'eutilis\'es

\end{itemize}

\end{slide}


%---------------------------------------------------------------------
%                       La philopsophie ORME  (suite)                #8
%---------------------------------------------------------------------

\begin{slide}{}

\heading{La construction d'une bonne complétion (suite)}


\begin{itemize}

\item L'\emph{efficacit\'e\/} est obtenue par des optimisations de haut niveau, 

\item La \emph{lisibilit\'e\/} rend le programme facile \`a ma{\^\i}triser,

\item Les \emph{optimisations de bas niveau\/} sont obte\-nues au niveau
de la bo{\^\i}te \`a outil,

\item Quand on aura obtenu un programme rai\-son\-nable\-ment efficace, le
programme CAML pourra servir de \emph{documentation\/} pour une
implantation rapide.


\end{itemize}

\end{slide}
%%------------------------------------------------------
%\begin{slide}
%  \begin{center}
%    {\large \bf \color{brunfonce}{\textit{Différentes procédures de complétion}}}
%\end{center}
%\end{slide}
%%--------------------------------------------------------------------------
%\begin{slide}
%\subheading{KB completion}
%\begin{scriptsize}
%\begin{verbatim}
%let rec KB_Completion ordering (R,E) = 

%    match E with
    
%        [] -> (R, []) C  (* succes *)
    
%     | (_::_) ->  KB_Completion ordering ((repeat Delete)
%                                         ((repeat Simplify) 
%                                         (Deduction 
%                                         ((repeat Collapse)
%                                         ((repeat Compose)
%                                         ((Orient ordering) (R, E)))))))


%\end{verbatim}
%\end{scriptsize}
%\end{slide}
%%--------------------------------------------------------------------------
%\begin{slide}
%\emph{Deduction} calcule toutes les paires critiques entre les
%identités de~\bleu{E_j}.
%\end{slide}

%%------------------------------------------------------------------------
%%               KB-COMPLETION (figure)
%% -----------------------------------------------------------------------

%\begin{slide}{}
%\setlength{\unitlength}{0.0125in}%
%\begin{picture}(260,100)(20,720)
%\thicklines
%\put( 20,720){\framebox(140,40){}}
%\put( 20,780){\framebox(180,40){}}
%\put(280,740){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{R}}}
%\put(280,800){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{E}}}
%\end{picture}

%\end{slide}

%% --------------------------------------------------------------------------
%%                       LA KB-COMPLETION
%% --------------------------------------------------------------------------


%\begin{slide}{}
%L'implantation de la proc\'edure  de Knuth et Bendix
%\begin{itemize}
%    \item poss\`ede un \rouge{contr\^ole tr\`es simple et \'equitable}, 
%    \item mais elle est  \rouge{inefficace}.
%\end{itemize}

%\end{slide}


%%---------------------------------------------------------------------------
%%                       LA N-COMPLETION
%%--------------------------------------------------------------------------


%\begin{slide}{}
%\heading{La N-complétion}

%La \emph{KB-complétion\/} est co\^{u}teuse car elle calcule toutes les
%paires critiques \`{a} chaque boucle. 

%Il est pr\'{e}f\'{e}rable de \emph{calculer les paires critiques entre
%deux r\`{e}gles \`{a} la fois\/} et de s'arranger pour ne plus jamais
%les recalculer.

%\vfill
%\end{slide}


%%---------------------------------------------------------------------------
%%                       LA N-COMPLETION (suite)
%%--------------------------------------------------------------------------


%\begin{slide}{}
%\heading{La N-complétion (suite)}

%Cela n\'{e}cessite la structure de donn\'{e}es suivante:
%\begin{itemize}
%  \item \bleu{E} est \emph{un ensemble d'identit\'{e}s\/}, ou bien
%paires critiques ou bien identit\'{e}s donn\'{e}es au d\'{e}part.
%\item \bleu{T} est un ensemble de r\`{e}gles, \emph{les r\`{e}gles non
%marqu\'{e}es\/} dans la terminologie de Huet, \item \bleu{R} est un
%ensemble de r\`{e}gles dont \emph{les paires critiques ont \'{e}t\'{e}
%calcul\'{e}es\/}, \emph{les r\`{e}gles marqu\'{e}es\/}
%\end{itemize}
%\vfill
%\end{slide}

%%------------------------------------------------------------------------
%%               N-COMPLETION (programme)
%% -----------------------------------------------------------------------
%\begin{slide}
%\subheading{N complétion}
%\begin{tiny}
%\begin{verbatim}
%let rec N_Completion ordering (R,T,E) = let COMP = N_Completion ordering in
%match (T,E) with
%    [],[] ->  (R,[],[]) C{(* success *)

% |  (_::_),[] -> COMP (Deduction 
%                      (repeat_list [Collapse_T_by_T;
%                                    Collapse_T_by_R;
%                                    Collapse_R_by_T;
%                                    Collapse_R_by_R;
%                                    Compose_T;
%                                    Compose_R] (R,T,E)))

% |  _,(_::_) -> let (R',T',E') = repeat_list[Delete;
%                                             Simplify](R,T,E) in
%                 (match E' with 
%                      [] -> COMP(R',T',E')
%                    | (_::_) -> COMP(Orient ordering (R',T',E') 
%                                ? failwith "non orientable equation"));;
%\end{verbatim}
%\end{tiny}
%\end{slide}
%%------------------------------------------------------------------------
%%               N-COMPLETION (figure)
%% -----------------------------------------------------------------------

%\begin{slide}{}
%\setlength{\unitlength}{0.0125in}%
%\begin{picture}(260,160)(20,660)
%\thicklines
%\put( 20,660){\framebox(160,40){}}
%\put( 20,720){\framebox(140,40){}}
%\put( 20,780){\framebox(180,40){}}
%\put(280,685){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{R}}}
%\put(280,740){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{T}}}
%\put(280,800){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{E}}}
%\end{picture}

%\end{slide}

%% ------------------------------------------------------------------------
%%               S-COMPLETION
%% -----------------------------------------------------------------------

%\begin{slide}{}
%\begin{center}
%\heading{La S-complétion}
%\end{center}
%Structure de donn\'{e}es
%\begin{itemize}
%  \item \bleu{E} comme dans la \emph{N-complétion\/},
%  \item \bleu{S} un ensemble d'identit\'{e}s ordonn\'{e}es ou r\`{e}gles qui
%sont utilis\'{e}s pour simplifier les autres identit\'{e}s ou r\`{e}gles et
%qui sont appel\'{e}s des \emph{simplifieurs\/}.  Pendant la compl\'{e}tion
%\bleu{S} contient z\'{e}ro ou une r\`{e}gle,

%  \item \bleu{T} un ensemble de r\`{e}gles d\'{e}j\`{a} utilis\'{e}es pour
%simplifier, mais dont les paires critiques n'ont pas encore \'{e}t\'{e}
%calcul\'{e}es.

%  \item \bleu{R} comme dans la \emph{N-complétion\/}.
%\end{itemize}

%\end{slide}


%%------------------------------------------------------------------------
%%               S-COMPLETION (programme)
%% -----------------------------------------------------------------------
%\begin{slide}
%\subheading{S complétion}
%\begin{tiny}
%\begin{verbatim}
% let rec S_Completion ordering (R,T,S,E) = 
%                      let COMP = S_Completion ordering in 
%match (T,S,E) with
%    [],[],[] ->  (R,[],[],[]) C{(* success *)CE{

% |  _,(_::_),_  -> (COMP (R',T'@S',[],E')
%                     where R',T',S',E' =
%                          repeat_list [Collapse_T_by_S;
%                                       Compose_T_by_S;
%                                       Collapse_R_by_S;
%                                       Compose_R_by_S] (R,T,S,E))
% |  (_::_),[],[] -> COMP (Deduction (R,T,S,E))

% |  _,[],(_::_) -> let (R',T',S',E') = repeat_list[Delete;
%                                                   Simplify]  (R,T,S,E) 
%                   in (match E' with 
%                      [] -> COMP(R',T',S',E')
%                    | (_::_) -> COMP (Orient ordering (R',T',S',E') 
%                                 ? failwith "non orientable equation"));;


%\end{verbatim}
%\end{tiny}
%\end{slide}
%%------------------------------------------------------------------------
%%               S-COMPLETION (figure)
%% -----------------------------------------------------------------------

%\begin{slide}{}
%\setlength{\unitlength}{0.0125in}%
%\begin{picture}(260,220)(20,600)
%\thicklines
%\put( 20,600){\framebox(60,40){}}
%\put( 20,720){\framebox(40,40){}}
%\put( 20,660){\framebox(140,40){}}
%\put( 20,780){\framebox(180,40){}}
%\put(280,620){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{R}}}
%\put(280,675){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{T}}}
%\put(280,740){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{S}}}
%\put(280,800){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{E}}}
%\end{picture}

%\end{slide}

%% -------------------------------------------------------------------------
%%                       ANS-COMPLETION
%% -------------------------------------------------------------------------

%\begin{slide}{}
%\begin{center}
%\heading{L'ANS-complétion}
%\end{center}
%Structure de donn\'{e}es:
%\begin{itemize}
%  \item \bleu{E} comme dans la  \emph{S-complétion\/},
%  \item \bleu{S} comme dans la \emph{S-complétion\/},
 
% \item \bleu{T} est l'ensemble des r\`{e}gles venant de $S$ et attendant
% de rentrer dans $C$.

%\end{itemize}
%\end{slide}


%% -------------------------------------------------------------------------

%\begin{slide}{}
%\begin{center}
%\heading{L'ANS-complétion (suite)}
%\end{center}
%\begin{itemize}
%  \item \bleu{C} est un ensemble qui contient une ou z\'{e}ro r\`{e}gle et
%dont les paires critiques avec les r\`{e}gles de~$N$ doivent \^{e}tre
%calcul\'{e}es.

%  \item \bleu{N} est un ensemble de r\`{e}gles dont les paires
%critiques n'ont pas \'{e}t\'{e} calcul\'{e}es avec les r\`{e}gles de
%$C$, mais dont les paires critiques avec les r\`{e}gles de $A \cup N$
%ont \'{e}t\'{e} calcul\'{e}es.

%  \item \bleu{A} est un ensemble de r\`{e}gles dont les paires critiques
%avec celle de $A \cup N \cup C$ ont \'{e}t\'{e} calcul\'{e}es.

%\end{itemize}

%\end{slide}


%%------------------------------------------------------------------------
%%               S-COMPLETION (programme)
%% -----------------------------------------------------------------------
%\begin{slide}
%\subheading{\footnotesize ANS completion}
%\begin{tiny}
%\begin{verbatim}
%let rec ANS_Completion ordering (A,N,C,T,S,E) = 
%    let COMP = ANS_Completion ordering in

%match (N,C,T,S,E) with
%   _,[],[],[],[] -> (A,N,C,T,S,E) C{(* success *)

% | _,_,_,(_::_),_ -> (COMP (A',N',C',T'@S',[],E')
%            where A',N',C',T',S',E' =
%            repeat_list [Collapse_A_by_S;Compose_A_by_S;
%                         Collapse_N_by_S;Compose_N_by_S;
%                         Collapse_C_by_S;Compose_C_by_S;
%                         Collapse_T_by_S;Compose_T_by_S] 
%                                           (A,N,C,T,S,E))

% | _,_,_,[],(_::_) -> let  A',N',C',T',S',E' = 
%                                  repeat_list[Delete;
%                                              Simplify](A,N,C,T,S,E) in
%          (match E' with
%              [] ->  COMP(A',N',C',T',S',E')
%            | (_::_) ->  COMP(Orient ordering (A',N',C',T',S',E')
%                                ? failwith "non orientable equation"))

% | (_::_),[_],_,[],[] -> COMP (Deduction(A,N,C,T,S,E))

% | [],[_],_,[],[] -> COMP (A_C2N crit (Internal_Deduction (A,N,C,T,S,E)))

% | _,[],(_::_),[],[] -> (COMP([],A@N,[r],T',[],[]) 
%                                 where r,T' = least Size T);;
%\end{verbatim}
%\end{tiny}
%\end{slide}
%% -------------------------------------------------------------------------
%%                       ANS-COMPLETION (figure)
%% -------------------------------------------------------------------------
%\begin{slide}{}
%\setlength{\unitlength}{0.0125in}%
%\begin{picture}(260,400)(20,420)
%\thicklines
%\put( 20,720){\framebox(40,40){}}
%\put( 20,580){\framebox(40,40){}}
%\put( 20,420){\framebox(220,40){}}
%\put( 20,500){\framebox(100,40){}}
%\put( 20,660){\framebox(140,40){}}
%\put( 20,780){\framebox(180,40){}}
%\put(280,435){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{A}}}
%\put(280,515){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{N}}}
%\put(280,595){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{C}}}
%\put(280,675){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{T}}}
%\put(280,740){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{S}}}
%\put(280,800){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{E}}}
%\end{picture}

%\end{slide}
%% -------------------------------------------------------------------------
%%               RESUME
%% -------------------------------------------------------------------------

%\begin{slide}{}
%\heading{En R\'ESUM\'E}

%\begin{description}
%\item[\emph{La KB-complétion}] est simple et poss\`{e}de un contr\^{o}le
%\'{e}quitable, mais elle calcule trop de paires critiques,

%\item[\emph{La N-complétion}] calcule moins de paires critiques, mais
%ne fait pas assez de simplifications 

%\item[\emph{La S-complétion}] conf\`{e}re aux simplifications une
%haute priorit\'{e}, 

%\item[\emph{L'ANS-complétion}] calcule encore moins de paires
%critiques et fait plus de simplifications,

%\item[\emph{L'ANIS-complétion}] calcule une paire critique \`{a} la
%fois. 

%\end{description}

%\end{slide}

%% -------------------------------------------------------------------------

%\begin{slide}{}
%\begin{center}
%\begin{tabular}{||c||}\hline\hline
%Ces proc\'{e}dures peuvent \'{e}chouer\\
%sur des identit\'{e}s non orientables.
%\\ \hline\hline
%\end{tabular}
%\end{center}

%\end{slide}
%%-------------------------------------------------------------------------
%%                       STATISTIQUES
%% -------------------------------------------------------------------------

%\begin{slide}{}
%\heading{STATISTIQUES}
%\begin{center}
%\emph{Associativit\'{e} et Endomorphisme ou Distributivit\'{e}}
%\end{center}

%\begin{tabular}{||c|| r|r|r || r|r|r ||}
%\hline\hline
%\emph{Proc\'{e}dures} & \multicolumn{2}{c}\verdir{Assoc+Endo} & &
%\multicolumn{2}{c}\verdir{Assoc+Dist} &\\
%%
%\cline{2-7}
%%
%&\multicolumn{2}{c}{\em filtrages}& &\multicolumn{2}{c}{\em
%filtrages} & \\
%\cline{2-4}\cline{5-7}

% & {\tiny \em suc} & {\tiny \em \'{e}chec} & {\tiny \em pc} &
%{\tiny \em suc} & {\tiny \em \'{e}chec} & {\tiny \em pc} \\
%%
%\cline{1-7}\cline{1-7}
%%
%KB-completion & 16 & 575 & 7 & 19 & 771 & 8 \\
%%
%\hline
%%
%N-completion & 12 & 247 & 5 & 12 & 243 & 5 \\
%%
%\hline
%%
%S-completion & 12 & 168 & 5 & 12 & 148 & 5 \\
%%
%\hline
%%
%ANS-completion & 12 & 129 & 5 & 12 & 148 & 5 \\
%\hline\hline
%\end{tabular}
%\end{slide}

%% -------------------------------------------------------------------------

%\begin{slide}{}
%\heading{STATISTIQUES (suite)}
%\begin{center}
%\emph{Groupes}
%\end{center}

%\begin{tabular}{||c|| r|r|r ||}
%\hline\hline
%\emph{Proc\'{e}dures} & \multicolumn{2}{c}\emph{Groupes}& \\
%%
%\cline{2-4}
%%
%&\multicolumn{2}{c}\emph{filtrages}& \\
%\cline{2-4}

% & {\tiny \em succ\`{e}s} & {\tiny \em \'{e}chec} & {\em pc} \\
%%
%\cline{1-4}\cline{1-4}
%%
%KB-completion & 1,080 & 9,540 & 496  \\
%%
%\hline
%%
%N-completion & 220 & 4,486 &109 \\
%%
%\hline
%%
%S-completion & 171 & 3,490 & 84 \\
%%
%\hline
%%
%ANS-completion & 98 & 1,499 & 55 \\
%\hline\hline
%\end{tabular}

%\begin{center}
%\emph{Groupes avec division \`{a} droite}
%\end{center}
%\vskip 6pt
%\begin{tabular}{||c|| r|r|r ||}
%\hline\hline
%\emph{Proc\'{e}dures} & \multicolumn{2}{c}\emph{Groupes avec division} 
%&\\
%%
%\cline{2-4}
%%
%&\multicolumn{2}{c}\emph{filtrages}& \\
%\cline{2-4}

% &{\tiny \em succ\`{e}s} & {\tiny \em \'{e}chec} & \emph{pc} \\
%%
%\cline{1-4}\cline{1-4}
%%
%KB-completion & 1300 & 575,720 & 647 \\
%%
%\hline
%%
%N-completion  & 364 & 11,518 & 252 \\
%%
%\hline
%%
%S-completion  & 250 & 9,719 & 102 \\
%%
%\hline
%%
%ANS-completion  & 178 & 4,967 & 76 \\
%\hline\hline
%\end{tabular}

%\end{slide}

%% -------------------------------------------------------------------------

%\begin{slide}{}
%\heading{STATISTIQUES (suite)}
%\begin{center}
%\emph{Axiomes de Taussky}
%\end{center}
%\begin{tabular}{||c|| r|r|r ||}
%\hline\hline
%\emph{Proc\'{e}dures} & \multicolumn{2}{c}\emph{Taussky} & \\
%%
%\cline{2-4}
%%
%&\multicolumn{2}{c}\emph{filtrages}& \\
%\cline{2-4}

% & {\tiny \em succ\`{e}s} & {\tiny \em \a'{e}chec} & \emph{pc} \\
%%
%\cline{1-4}\cline{1-4}
%%
%KB-completion & \_ &\_ &\_\\
%%
%\hline
%%
%N-completion & 464 & 21,987 &194 \\
%%
%\hline
%%
%S-completion & 445 & 15,648 & 183 \\
%%
%\hline
%%
%ANS-completion & 324 & 9,292 & 139 \\
%\hline\hline
%\end{tabular}

%\end{slide}
%%

%% -------------------------------------------------------------------------
%%                        Mesures                          
%% -------------------------------------------------------------------------

%\begin{slide}{}
%\begin{center}
%\heading{ Mesures}
%\end{center}

%\begin{center}
%\begin{tabular}{||c|| r ||}
%\hline\hline
%{\it Exemples\/} & {\it Temps\/} \\
%\hline\hline
%Distributivit\'{e} & 0.18~s\\
%\hline
%Groupes & 6 s\\
%\hline
%Naturels & 4.4 s\\
%\hline
%Anneaux bool\'{e}ens & 17 s\\
%\hline
%Groupes ab\'{e}liens & 28 s\\
%\hline
%Anneaux & 150 s\\
%\hline\hline
%\end{tabular}
%\end{center}
%\end{slide}
%% -------------------------------------------------------------------------
%%                                       LES AXIOMES
%% ------------------------------------------------------------------------

%\begin{slide}{}

%\rouge{Associativit\'{e} + endomorphisme}
%\begin{eqnarray*}
%(x * y) * z & \ = \ & x * (y * z)\\
%f(x) * f(y) &\ = \ & f(x * y)
%\end{eqnarray*}

%\rouge{Associativit\'{e} + distributivit\'{e}}
%\begin{eqnarray*}
%(x + y) + z & \ = \ & x + (y + z)\\
%(x * y) + (x * z)  &\ = \ & x *(y + z)
%\end{eqnarray*}
%\end{slide}

%\begin{slide}{}
%\rouge{Groupes}
%\begin{eqnarray*}
%(x * y) * z & \ = \ & x * (y * z)\\
%e * x & \ = \ & x\\
%i(x) * x & \ = \ & e
%\end{eqnarray*}
%\end{slide}

%\begin{slide}{}
%\rouge{Groupes (système complété)}
%\begin{scriptsize}
%\begin{eqnarray*}
%(x * y) * z & \ \ra \ & x * (y * z)\\
%e * x & \ \ra \ & x\\
%x * e & \ \ra \ & x\\
%i(x) * x & \ \ra \ & e\\
%x * i(x) & \ \ra \ & e\\
%i(i(x)) & \ \ra \ & x\\
%i(e)  & \ \ra \ & e \\
%i(x * y)  & \ \ra \ & i(y) * i(x)\\
%x * (i(x) * y) & \ \ra \ & y \\
%i(x) * (x * y) & \ \ra \ & y
%\end{eqnarray*}
%\end{scriptsize}
%\end{slide}

%\begin{slide}{}
%\rouge{Groupes avec divison \`{a} droite}
%\begin{eqnarray*}
%(x * y) * z & \ = \ & x * (y * z)\\
%e * x & \ = \ & x\\
%i(x) * x & \ = \ & e\\
%x * i(y) & \ = \ & x / y
%\end{eqnarray*}

%\begin{eqnarray*}
%x * y  & \ \ra \ & x / i(y)\\[5pt]
%x / e  & \ \ra \ & x\\
%e / x  & \ \ra \ & i(x)\\
%i(e)  & \ \ra \ & e\\
%i(i(x)) & \ \ra \ & x\\
%i(x / y)& \ \ra \ & y / x\\
%x / x & \ \ra \ & e\\
%x / (y / z) & \ \ra \ & (x / i(z)) / y\\
%(x / y) / i(y) & \ \ra \ & x\\
%(x / i(y)) / y & \ \ra \ & x
%\end{eqnarray*}



%\end{slide}

\end{document}
% LocalWords:  joignables Taussky InvG InvD conservatif
