\documentclass[notes=none]{beamer}
\usepackage[T1]{fontenc}
\usepackage{pslatex}
\usepackage[french]{babel}
\usepackage{beamerthemeBoadilla}

\usecolortheme[rgb={.1,.5,.2}]{structure}
\setbeamertemplate{theorems}[ams style]
\setbeamercolor{titlelike}
	       {use={palette primary},fg=black,bg=palette
		 primary.bg} 


\input{p_entete}
\input{../aacs/macros_modified}
\input{sequents}

%\includeonly{pres_part2}
%\includeonlyframes{current}

\definecolor{lightblue}{rgb}{0,0.6,0.6}

\newcommand{\yeslogo}{\logo{\includegraphics[height=.07\textheight]{../aacs/loria.jpg}}}
\newcommand{\nologo}{\logo{}}

\title[Applications des S.C.A.]{Systèmes Canoniques
  Abstraits~:\\Application à la Complétion et \`a la D\'eduction Modulo}
\subtitle{S\'eminaire PROTHEO}
\author{Guillaume Burel}
\date[mars--novembre 2005]{Jeudi 3 Novembre 2005}
\institute[LORIA]{LORIA -- Équipe PROTHEO\\Encadrant : Claude Kirchner}
%\titlegraphic{\includegraphics[height=.2\textheight]{boule.jpg}}
\setbeamertemplate{caption}[numbered]
\logo{\includegraphics[height=.15\textheight]{../aacs/loria.jpg}}

\begin{document}
\begin{frame}
\titlepage
\end{frame}
\yeslogo

\part{Soutenance de stage de mast\`ere}

\frame{\partpage}

\yeslogo
\section{Introduction}
\begin{frame}
\frametitle{Introduction}

Démonstration automatique et interactive: de nombreux formalismes
logiques 
\begin{itemize}
\item\alert<5>{calcul des séquents} $\rightarrow$ calcul des constructions
[inductives, algébriques, \ldots]\pause

\item \alert<6>{complétion} [close,
  standard, modulo, \ldots]\pause

\item \alert<7>{résolution} [ordonnée, avec sélection,
  \ldots]\end{itemize}\pause
\medskip

Différentes représentations des preuves mais une notion commune:
certaines preuves sont «meilleures» que d'autres:\pause\ preuves sans
coupures\pause, preuves par réécriture\only<6>{ (en «vallée»)}\pause,
preuves qui appliquent la résolution sur les grands atomes en premier.
\medskip\pause

Cadre des systèmes canoniques abstraits (S.C.A.) introduit par \cite{acp}: la
notion de bonne preuve est traduite par un \alert{ordre sur les preuves}.

\end{frame}

\begin{frame}
\frametitle{Introduction}
  Cadre le plus général et formel possible $\rightarrow$ nécessité de
  vérifier qu'il correspond bien à des cas concrets.
\pause\bigskip

Systèmes de séquents $\rightarrow$ obligation de généraliser le cadre
\pause\bigskip

Complétion: formalisme autour duquel a été construit le cadre

Preuve non détaillée dans \cite{aci} pour la complétion close 

Preuve pour la complétion standard $\rightarrow$ représentation des
preuves
\end{frame}

\begin{frame}
\frametitle{Plan}
  \tableofcontents
\end{frame}

\AtBeginSection[]
{
   \begin{frame}
       \frametitle{Plan}
       \tableofcontents[currentsection]
   \end{frame}
}

\section{Présentation des S.C.A.}
\subsection{Définitions et Postulats}
\begin{frame}
\frametitle{Définitions}
\only<1>{\input{pres_1.pdf_t}}
\only<2>{\input{pres_2.pdf_t}}
\only<3>{\input{pres_3.pdf_t}}
\only<4>{\input{pres_4.pdf_t}}
\only<5>{\input{pres_first.pdf_t}}
\only<6>{\input{pres_proof.pdf_t}}
\only<7>{\input{pres_order.pdf_t}}
\only<8->{\input{pres_final.pdf_t}}

\onslide<9>{Pour les \emph{justifications}: $\bettereq$\\ Pour les
  \emph{présentations}: $\simpler$}
\end{frame}

\begin{frame}
\frametitle{Postulats}
$$\Th A~\df~\Cl{\Pf A}$$
\pause

\begin{fpost}[Réflexivité]\label{post:frefl}
  Pour toute présentation $A$:
  $$ A\subseteq \Th A$$
\end{fpost}
\pause

\begin{fpost}[Fermeture]\label{post:fermeture}
  Pour toute présentation $A$:
  $$ \Th{\Th A}\subseteq \Th A$$
\end{fpost}
\end{frame}

\begin{frame}[label=sp]
\frametitle{Sous-preuves}

On définit aussi une notion de sous-preuve sur $\P$ notée $\rhd$.
\begin{center}\input{pres_sp.pdf_t}\end{center}
\bigskip

Preuve triviale $\triva a$ telle que $\Ax{\triva a }=\{\Cl{\triva
  a}\}=\{a\}$ et $\forall q.~\triva a\ntriangleright q$

\end{frame}

\nologo
\begin{frame}<1-2>[label=post]
\frametitle{Postulats}
\begin{fpost}[Trivia]\label{post:hyp_sp}
  Pour toute preuve $p$ et toute formule $a$:
  $$a\in\Ax p \imp p\unrhd\triva a$$
\end{fpost}
\pause

\begin{fpost}[Monotonie des Hypothèses des Sous-Preuves]
  \label{post:hyp_mono}
  Pour toutes preuves $p$ et $q$:
  $$p\unrhd q\imp \Ax p\supseteq \Ax q$$
\end{fpost}
\pause

\begin{fpost}[Remplacement]\label{post:remplacement}
  Pour toutes preuves $p$, $q$ et $r$:
  $$p\rhd q > r \imp \exists v\in \Pfa{\Ax p\cup\Ax r}.~ p > v\rhd r$$
\end{fpost}
\end{frame}
\yeslogo

\begin{frame}
\frametitle{Postulat E}

\begin{center}\input{pres_remp.pdf_t}\end{center}


\end{frame}

\againframe<3>{post}

\subsection{Présentation Canonique}
\begin{frame}
\frametitle{Présentation Canonique}

$$A^\sharp~\df~\Ax{\mu\Pf{\Th A}}$$
\pause

\begin{center}
\parbox[B]{.4\textwidth}{
$$\mu\Pf{\Th{A^\sharp}}\subseteq{\Pf{A^\sharp}}$$
\center{Notion de \emph{saturation}}
 }\pause+
\parbox[B]{.4\textwidth}{
$$\forall r\in A^\sharp.~A^\sharp\not\simpler
    A^\sharp\setminus \{r\}$$
\center{Notion de \emph{(non)-redondance}}
 }
\end{center}
\end{frame}

\subsection{Mécanismes de Déduction}
\begin{frame}
\frametitle{Mécanismes de Déduction}

Mécanisme de déduction: $\infers : 2^\A\rightarrow 2^\A$
\medskip

Limite: $A_\infty \df \liminf_{j\rightarrow\infty} A_j ~=~ \bigcup\limits_{j>0}
\bigcap\limits_{i>j} A_i$
\pause\bigskip

Adéquat et sain: $A\infers B\text{ implique } \Th A = \Th B$\pause\medskip

Bon: $A\infers B\text{ implique } A\simpler B$\pause\medskip

Canonique: $A_\infty=A_0^\sharp$
\end{frame}

\section{Systèmes ne préservant pas les Hypothèses}

\subsection{Déduction Naturelle et Postulat D}
\begin{frame}
\frametitle{Déduction Naturelle et Postulat \ref{post:hyp_mono}}
\begin{beamerboxesrounded}[shadow=true]{\textbf{Déduction
Naturelle}}
\begin{center}
\begin{tabular}{@{}p{.5\textwidth}@{}p{.5\textwidth}@{}}
  \Rule{Axiom:}
  $$\Axiom{\Gamma,A\seq A}$$
&\alert<2>{\Rule{Abstraction ($\limp$Introduction):}
  $$\Abs{\Gamma\seq A\limp B}{\Gamma, A\seq
  B}$$}
\end{tabular}

  \Rule{Application ($\limp$Elimination):}
  $$\App{\Gamma\seq B}{\Gamma\seq A\limp B}{\Gamma\seq A}$$
\end{center}
\end{beamerboxesrounded}
\end{frame}


\subsection{Généralisation des Postulats}

\def\thefpost{E$_{\mathsf{gen}}$}
\begin{frame}
\frametitle{Nouveau Cadre} Plus de postulat \ref{post:hyp_mono}
\pause\bigskip

Postulat \ref{post:remplacement} modifié:
\begin{fpost}[Remplacement Généralisé]

  \label{post:genRemplacement}
  Pour toute preuve $p$, $q$ et $r$:
 $$  p\rhd q > r \imp \exists v\in \Pfa{\Ax p\cup(\Ax r\alert{\setminus\Ax
  q})}.~ p > v\rhd r$$
\end{fpost}

\end{frame}

\begin{frame}
\frametitle{Exemple}
$
\Abs{\seq A\limp B\limp A}{\alert<2>{\mbox{
\Abs{\alert<5>{A}\seq B\limp A}{\Axiom{\alert<5>{A},B\seq A}}}}}$%
\onslide<3->\ donne 
\only<3>{$\Abs{\seq A\limp B\limp A}{\alert<3>{\mbox{
\Axiom{B\limp A,A\seq B\limp A}}}}$}
\only<4->{$\Abs{\alert<4>{B\limp A}\seq A\limp B\limp A}{\Axiom{B\limp
      A,\alert<5>{A}\seq B\limp A}}$}
\onslide<5->
\bigskip

La preuve résultante est bien dans \only<5>{$\Pf{\Ax p\cup(\Ax r\alert{\setminus(\Ax
  q\setminus\Ax p)})}$}\only<6>{$\Pf{\Ax p\cup(\Ax r\alert{\setminus\Ax
  q})}$}\only<7>{$\Pf{\emptyset\cup(\{B\limp
  A,A\}\setminus\{A\})}$}\only<8>{$\Pf{\{B\limp A\}}$}.

\end{frame}

\section{Application à la Complétion}
\subsection{Présentation}

\begin{frame}
  \frametitle{Application à la Complétion}
 
Deux procédures de complétions ont été étudiées:
\begin{itemize}
  \item complétion close; preuve complète et détaillée, contrairement
  à celle de \cite{DershowitzFTP2003,aci}
\item complétion standard; nécessité de comparer plusieurs
  représentations de preuves
\end{itemize}

\end{frame}


\begin{frame}[label=p_KB]
\frametitle{Complétion Standard}
  La complétion standard a été introduite par \cite{KnuthBendix70}
\medskip

Transforme un ensemble d'axiomes équationnels en un système de
réécriture confluent et terminant
\bigskip

Complétude démontrée pour la première fois par
\cite{HuetCompletionINRIA}
\bigskip

Peut être représentée par des règles d'inférences, par exemple
\cite{Bachmair-87}
\hyperlink{CS}{\beamergotobutton{Règles d'inférence}}

\end{frame}

\nologo
\subsection{Représentations des Preuves}
\begin{frame}
  \frametitle{Termes de Preuve}

\begin{beamerboxesrounded}[shadow=true]{\textbf{Règles de Formation
      des Termes de Preuve} \cite{MeseguerTCS92}}
\begin{center}
\begin{tabular}{@{}p{.6\textwidth}@{}p{.4\textwidth}@{}}
\Rule{Congruence:}
$$\infer{f(\vect\pi):f(\vect t)\rewrite f(\vect{t'})}
{\pi_1:t_1\rewrite t_1' &\ldots & \pi_n:t_n\rewrite t_n'}$$
&
\Rule{Transitivité:}
$$\infer{\pi_1;\pi_2:t_1\rewrite t_3}
{\pi_1:t_1\rewrite t_2 & \pi_2:t_2\rewrite t_3}$$
\\
\Rule{Remplacement:}

$\ell:(g(\vect x),d(\vect x))\in E\cup R$
$$\infer{\ell(\vect\pi):g(\vect t)\rewrite d(\vect{t'})}
{\pi_1:t_1\rewrite t_1' &\ldots & \pi_n:t_n\rewrite t_n'}$$
 
&
\Rule{Symétrie:}
$$\infer{\pi^{-1}:t_2\rewrite t_1}
{\pi:t_1\rewrite t_2}$$
\end{tabular}
\end{center}
\end{beamerboxesrounded}


\end{frame}
\yeslogo
\begin{frame}

\frametitle{Preuves par Remplacement}

Introduites par \cite{Bachmair-87} pour montrer la complétude la
complétion standard

Étape de preuve équationnelle: $\epfstep s{u=v}pt$ 

avec
$\subterm s p =\sigma(u)$ et $t=\replacement s{\sigma(v)}p$
\pause\medskip

Étape de preuve par réécriture: $\rpfstep s{u\rightarrow v}pt$ ou
$\lpfstep t{u\rightarrow v}ps$

avec
$\subterm s p =\sigma(u)$ et $t=\replacement s{\sigma(v)}p$
\pause\bigskip

Preuve par remplacement:
$$\upfstep [0]{s_0} {\ell_0} {p_0} {\upfstep [1]{s_1} {\ell_1} {p_1}
  {s_2\cdots\upfstep [n]{s_n} {\ell_n} {p_n} {t_n}}}$$
avec $\upfstep[i]{}{}{}{}\in\{\epfstep{}{}{}{},\rpfstep{}{}{}{},\lpfstep{}{}{}{}\}$

\end{frame}

\begin{frame}
  \frametitle{Des Termes de Preuve aux Preuves par Remplacement}
Si $\pi=f(\ell_1(\ell_2),(\ell_3;r)^{-1})$ où $\ell_1 : g(x)\rewrite
d(x)$, $\ell_2 : s=t$, $\ell_3:l\rewrite r$, on a:\\\pause
\begin{tabular}{r@{$~\rewrite[\ptrs/\assoc]~$}l@{\hspace{.5cm}}l}$\pi$&
$f(\ell_1(s);d(\ell_2),(\ell_3;r)^{-1})$&(\Rule{Mouvements
Parallèles})\\\pause
&$f(\ell_1(s);d(\ell_2), r); f(d(t),(\ell_3;r)^{-1})$&
(\Rule{Séquençage})\\\pause
&$f(\ell_1(s);d(\ell_2), r); f(d(t), r^{-1};\ell_3^{-1})$&
(\Rule{Inversion de la Composition})\\\pause
&$f(\ell_1(s);d(\ell_2), r); f(d(t), r;\ell_3^{-1})$\\\multicolumn{3}{c}
{(\Rule{Suppression des Inverses Inutiles})}\\\pause
&$f(\ell_1(s);d(\ell_2), r); f(d(t), \ell_3^{-1})$\\\multicolumn{3}{c}
{(\Rule{Suppression des Identités Inutiles})}\\\pause
&$f(\ell_1(s),r);f(d(\ell_2), r); f(d(t), \ell_3^{-1})$&
(\Rule{Remontée de la Composition})\\\pause
&$f(\ell_1(s),r);f(d(\ell_2), r); f(d(t), \ell_3)^{-1}$&
(\Rule{Inversion de la Congruence})
\end{tabular}\pause
\bigskip

$\rpfstep{f(g(s),r)}{\ell_1}1{\epfstep{f(d(s),r)}{\ell_2}{11}{\lpfstep{f(d(t),r)}{\ell_3}2{f(d(t),l)}}}$

\end{frame}

\subsection{Ordre sur les preuves}

\begin{frame}
  \frametitle{Ordre sur les preuves}
Ordre sur les preuves par remplacement \cite{Bachmair-87}:

Coût de $\epfstep s{u=v}pt$: $(\lmbra
s,t\rmbra,u,t)$

 Coût de $\rpfstep s{u\rightarrow v}pt$: $(\lmbra
s\rmbra,u,t)$

Coût d'une preuve par remplacement: multiensemble des coûts de 
ses étapes.
\pause\bigskip

Ordre sur les termes de preuves:

Un terme de preuve $p$ est supérieur à un autre $q$ si\\
le coût de la forme
normale de $p$ pour $\ptrs/\assoc$ est supérieur à celui de la forme
normale de $q$.
\end{frame}


\subsection{La Complétion Standard comme Instance des S.C.A.}
\begin{frame}
  \frametitle{Vérification des Postulats}

Postulats A B C D: pas de problèmes.
\bigskip

Postulat E:
\begin{ftheo}[Postulat \ref{post:remplacement} pour les Preuves Équationnelles]
  Pour tous termes de preuves $p,r$, pour toute position $i\in\position p$,

$$\subterm p i>r\text{ implique } p>\replacement p r i$$
\end{ftheo}
\end{frame}

\begin{frame}
  \frametitle{La Complétion Standard est Canonique}
La complétion standard est \alert<1>{saine et adéquate}:
\cite[lemme 2.1]{Bachmair-87}\pause\medskip 

La complétion standard est \alert<2>{bonne}:
\cite[lemmes 2.5, 2.6]{Bachmair-87}\pause\medskip

La complétion standard est \alert<3>{canonique}:
\begin{ftheo}
  Pour toute dérivation $\left(E_i,R_i\right)_i$ de la complétion
  standard qui \emph{termine sans échec},
  $$R_\infty~=~E_0^\sharp$$
\end{ftheo}

\end{frame}

\section{Conclusion}
\begin{frame}
  \frametitle{Conclusion}
On a pu appliquer les systèmes canoniques abstraits:
\begin{itemize}[<+->]
  \item à la déduction naturelle, grâce à une \alert<3>{généralisation
  du cadre} pour les systèmes de preuve ne préservant pas les
  hypothèses dans les sous-preuves; 

preuves minimales = 
  preuves sans coupures
\item aux \alert<4>{complétions close et standard}, pour lesquelles une preuve
  complète et détaillée est donnée.
\end{itemize}
\medskip

\onslide<3->
Ces résultats sont probablement extensibles au calcul des séquents, à
la logique linéaire\pause, à la complétion modulo, à l'algorithme de
Buchberger.\pause\medskip

Calcul des constructions, calcul des séquents modulo, procédure de
résolution ?\pause\bigskip

Ordres différents sur les systèmes de séquent\pause\medskip

Formalisation en Coq
\end{frame}

\part{D\'eduction Modulo Asym\'etrique}

\frame{\partpage}

\begin{frame}
\frametitle{Plan}
  \tableofcontents
\end{frame}

\section{D\'eduction Modulo et R\'e\'ecriture}
\subsection{Introduction \`a la D\'eduction Modulo}
\begin{frame}
  \frametitle{La D\'eduction Modulo}

Principe de Poincar\'e: diff\'erence entre d\'emonstrations de 
\medskip

\begin{tabular}{rcl}$2+2
=4$ & et & Axiome du choix $\Leftrightarrow$ Lemme de Zorn\\
calcul &$\neq$ &raisonnement
\end{tabular}
\bigskip

En d\'eduction modulo \cite{DHK-TPM-JAR}, les \'etapes de calcul sont
masqu\'ees pour faire appara\^itre le raisonnement.
\end{frame}

\begin{frame}
\frametitle{Calcul des S\'equents Modulo}

R\`egles de conversion:
$$\Convg\Gamma\Delta A B \quad\text{ si }A\equiv B\quad\Convd\Gamma\Delta A B$$


\onslide<2>{\begin{beamerboxesrounded}[shadow=true]{\textbf{Calcul des S\'equents Modulo}}
\begin{columns}
\column{.5\textwidth}
$$\Axiomm\Gamma\Delta A B\text{ si }A\equiv B$$
$$\Notd\Gamma\Delta A B\text{ si }A\equiv\neg B$$
$$\Andd\Gamma\Delta A B C\text{ si }A\equiv B\wedge C$$
$$\Exd\Gamma\Delta A B t x\text{ si }A\equiv \exists x.~B$$

\column{.5\textwidth}
$$\Cut\Gamma\Delta A B\text{ si }A\equiv B$$
$$\Impd\Gamma\Delta A B C\text{ si }A\equiv B\imp C$$
$$\Ord\Gamma\Delta A B C\text{ si }A\equiv B\vee C$$
$$\Alld\Gamma\Delta A B c x\text{ si }A\equiv \forall x.~B$$
\flushright et $c$ constante fra\^iche

\end{columns}

\end{beamerboxesrounded}}

\end{frame}

\begin{frame}
  \frametitle{D\'eduction Modulo Asym\'etrique \cite{DBLP:conf/rta/Dowek03}}

Congruence $\equiv$ simul\'ee par un syst\`eme de r\'e\'ecriture $\limp$
\pause\bigskip


Analycit\'e $\imp$ on ne r\'e\'ecrit que vers le haut

R\`egles de conversion:
$$\Upg\Gamma\Delta A B \quad\text{ si }A\limp B\quad\Upd\Gamma\Delta A B$$


\onslide<2>{\begin{beamerboxesrounded}[shadow=true]{\textbf{Calcul des
	S\'equents Modulo Asym\'etrique}}
\begin{columns}
\column{.5\textwidth}
$$\Axiomm\Gamma\Delta A B\text{ si }A\ra^*\la^* B$$
$$\Notd\Gamma\Delta A B\text{ si }A\ra^*\neg B$$
$$\Andd\Gamma\Delta A B C\text{ si }A\ra^* B\wedge C$$

\column{.5\textwidth}
$$\Cut\Gamma\Delta A B\text{ si }A\la^*\ra^* B$$
$$\Ord\Gamma\Delta A B C\text{ si }A\ra^* B\vee C$$
$$\Alld\Gamma\Delta A B c x\text{ si }A\ra^* \forall x.~B$$
\flushright et $c$ constante fra\^iche

\end{columns}
\end{beamerboxesrounded}}

\end{frame}

\subsection{Rappels de R\'e\'ecriture}
\begin{frame}
  \frametitle{R\'eduction de Pics et Confluence}

Confluence: \input{confluence.pdf_t}
\pause

Algorithme de Newman de r\'eduction de pics \cite{Newman42}:
\only<2>{\input{newman1.pdf_t}}
\only<3>{\input{newman2.pdf_t}}
\only<4>{\input{newman3.pdf_t}}

\end{frame}

\begin{frame}
  \frametitle{Confluence $\not\imp$ R\'eduction de Pics}

Contre-exemple:
\begin{center}
  \input{contrex_newman.pdf_t}
\end{center}
\bigskip

%\begin{center}
\only<2,5->{\input{cen1.pdf_t}}%
\only<3>{\input{cen2.pdf_t}}%
\only<4>{\input{cen3.pdf_t}}%
\only<5-7>{$\quad\rightsquigarrow\quad$}%
\only<8->{$\quad\leftrightsquigarrow\quad$}%
\only<5>{\input{cen4.pdf_t}}%
\only<6,8>{\input{cen5.pdf_t}}%
\only<7>{\input{cen6.pdf_t}}%
%\end{center}

\end{frame}

\subsection{Confluence et \'Elimination des Coupures}
\begin{frame}
  \frametitle{R\'e\'ecriture sur les Termes Uniquement}

\begin{ftheo}
  $\Gamma\seq\Delta$ ssi $\exists A\in\Gamma,B\in\Delta$
  t.q. $A\lra^*B$
\end{ftheo}
\begin{overprint}%
\only<1>{%
\begin{proof}
$\imp$ par induction sur la preuve de $\Gamma\seq\Delta$

$\Leftarrow$ par induction sur le nombre de pics sur la preuve par
  remplacement de $A\lra^*B$, chaque pic est simul\'e par une r\`egle
  de coupure

\end{proof}
}%
\onslide<2->%
\begin{ftheo}
  $\Gamma\seq^{cf}\Delta$ ssi $\exists A\in\Gamma,B\in\Delta$
  t.q. $A\ra^*\la^* B$
\end{ftheo}

\begin{overprint}%
\only<2>{%
\begin{proof}
$\imp$ par induction sur la preuve de $\Gamma\seq^{cf}\Delta$

$\Leftarrow$ on a $\Axiomm\Gamma\Delta A B$

\end{proof}
}%
\onslide<3->{

\begin{fcoro}
  confluence $\Leftrightarrow$ \'elimination des coupures
\end{fcoro}}
\end{overprint}
\end{overprint}


\end{frame}

\begin{frame}
  \frametitle{R\'e\'ecriture sur les Propositions}

Il est possible de r\'e\'ecrire des propositions atomiques :
$$x*y=0 \limp x = 0\vee y=0$$
\pause

On a plus confluence $\Rightarrow$ \'elimination des coupures :
contre-exemple de Crabb\'e

$$ A\limp B\wedge \neg A$$

$$\infer[\neg\text{-d}]{\seq\neg B}{%
\infer[\text{Coup}]{B\seq}{%
\infer[\wedge\text{-g}]{B,A\seq}{%
\infer[\neg\text{-g}]{B,A,\neg A\seq}{%
\infer[\text{Axiome}]{B,A\seq A}{}}} &%
%
\infer[\wedge\text{-d}]{B\seq A}{%
\infer[\text{Axiome}]{B\seq B}{} &%
\infer[\neg\text{-d}]{B\seq\neg A}{%
\infer[\wedge\text{-g}]{B,A\seq}{%
\infer[\neg\text{-g}]{B,A,\neg A\seq}{%
\infer[\text{Axiome}]{B,A\seq A}{}%
}}}}}}$$

(terme de preuve $\lambda y.(\lambda x.(\text{snd}~x) x)<y,\lambda x.(\text{snd}~x) x>$)
\end{frame}

\begin{frame}
  \frametitle{R\'esum\'e}

\begin{columns}
\column{.4\textwidth}
\begin{center}
\textbf{R\'e\'ecriture}
\bigskip
  
\onslide<2->{R\'eduction de pics
\medskip}

\onslide<4->{$\Downarrow$\onslide<8->{$\not\Uparrow$}
\medskip

Confluence
\bigskip}


\onslide<9->{
$\upuparrows$
\medskip

Proc\'edure de compl\'etion}

\end{center}
\column{.1\textwidth}
\begin{center}
\textbf{\ }
\bigskip

\onslide<3->{$\Leftarrow$\onslide<8->{$\not\Rightarrow$}
\medskip}

\onslide<6->{\alert<6>{\rotatebox{135}{$\not\Rightarrow$}}%
\onslide<7->{\alert<7>{\raisebox{.4em}{\rotatebox{-45}{$\not\Rightarrow$}}}}%
} 
\medskip

\onslide<5->{$\Leftarrow$\onslide<8->{$\not\Rightarrow$}
\bigskip}

\ 
\medskip

\ 

\end{center}

\column{.5\textwidth}
\begin{center}
\textbf{D\'eduction Modulo}
\bigskip
  
\onslide<3->{Normalisation
\medskip}

\onslide<5->{$\Downarrow$\onslide<8->{$\not\Uparrow$}
\medskip

Propri\'et\'e d'\'elimination des coupures
\bigskip}


\onslide<10->{$\upuparrows$\medskip

Compl\'etion g\'en\'eralis\'ee ?}

\end{center}


\end{columns}

\begin{overlayarea}{\textwidth}{1em}
\only<6>{Contre-exemple de Newman}%
\only<7>{Contre-exemple de Crabb\'e}%
\end{overlayarea}

\end{frame}

\section{Compl\'etion G\'en\'eralis\'ee}
\subsection{Approche de G. Dowek}
\begin{frame}
\frametitle{M\'ethode de G. Dowek \cite{dowek:theory}}

Soit $\mathcal T$ une th\'eorie sans quantificateur
\pause

On la met sous forme clausale $\ptrs$ $\Gamma = \vect \psi$
\pause

Soit $\mathcal M$ un mod\`ele de $\Gamma$ 

Il existe un lit\'eral $\pm P\in \psi_1$ tel que $\mathcal
M\models \pm P$
\pause

\begin{itemize}
  \item  $\mathcal M\models P$: on consid\`ere les $\psi_i$ tels que $\psi_i =
  P\vee A_i$
$$ P\ra P\vee \neg A_1\vee\cdots\vee\neg A_n $$
\pause
  \item  $\mathcal M\not\models P$: on consid\`ere les $\psi_i$ tels que $\psi_i =
  \neg P\vee A_i$
$$ P\ra P\wedge A_1\wedge\cdots\wedge A_n $$

\end{itemize}
\pause

On supprime toutes les clauses utilis\'ees, et on recommence jusqu'\`a
ce qu'il n'y en ait plus
  
\end{frame}

\newcommand{\bottom}{\perp}
\setbeamercovered{transparent}

\begin{frame}
  \frametitle{Exemple}

Crabb\'e: 
\only<1>{$$A\Leftrightarrow (B\wedge\neg A)$$}%
\only<2>{$$(A\Rightarrow (B\wedge\neg A))\wedge((B\wedge\neg
  A)\Rightarrow A)$$}%
\only<3>{$$(\neg A\vee(B\wedge\neg A))\wedge(\neg(B\wedge\neg A)\vee
  A)$$}%
\only<4->{$$\onslide<-10>{\alert<6>{(\neg A\vee \alert<8>{B})}\wedge(\neg%
  A\only<9>{\alert{\vee\bottom}})\wedge}\onslide<-13>{\alert<11>{(\neg B\vee \alert<13>{A})}}$$}% 

\onslide+<5->
$\mathcal M$: $|A|\mapsto 0$, $|B|\mapsto 0$
\bigskip

\begin{itemize}
\item\onslide+<6->
$P = A$ \onslide+<7-> 

\alert<14>{$$A\ra \only<7-9>{A\wedge}\only<8-9>{B\wedge}\only<9>{\bottom}\only<10->{\bottom}$$}

\item\onslide+<11->
$P = B$ \onslide+<12-> 

\alert<14>{$$B\ra {B\wedge}\onslide+<13->{A}$$}

\end{itemize}
\onslide+<14-> Poss\`ede la propri\'et\'e d'\'elimination des coupures

\end{frame}

\setbeamercovered{invisible}
\subsection{Notre Approche}

\begin{frame}
  \frametitle{Preuves Critiques}
\begin{fdefi}[Preuves Critiques]\label{defi:critical}
  $p\in\mu\Pfa A$ est dite \emph{critique} si:
  \begin{itemize}[<+->]
    \item $p\not\in\mu\Pf{Th A}$
    \item $\forall q\lhd p.~q\in\mu\Pf{\Th A}$
  \end{itemize}
\end{fdefi}
\onslide<3->

\begin{ftheo}[\'Equit\'e de la Compl\'etion]
Si une bonne d\'erivation $\{A_i\}_i$ est telle que
 $$\Crit{A_\infty}\better\Pf {A_*}$$

alors elle est \emph{saturante}
\end{ftheo}

Id\'ee: rajouter toutes les conclusions des preuves critiques
\end{frame}

\begin{frame}<-7>
  \frametitle{Notre Approche par l'Exemple}
Crabb\'e: $A~\ra~B\wedge\neg A$
$$\infer[\text{Coup}]{\alert<6>{\onslide<5->{B}\seq}}{%
\infer[\uparrow\text{-d}]{\onslide<5->{B}\seq A}{%
\onslide<2->{\infer[\wedge\text{-d}]{\onslide<5->{B}\seq B\wedge\neg A,A}{%
{\onslide<4->{\alert<4>B}\seq B,A}%
& 
\infer[\neg\text{-d}]{\onslide<5->{B}\seq \neg A,A}{%
\infer[\text{Axiome}]{\onslide<5->{B,}A\seq A}{}}}}} &
\infer[\uparrow\text{-g}]{\onslide<5->{B,}A\seq}{%
\onslide<3->{\infer[\wedge\text{-g}]{\onslide<5->{B,}A,B\wedge\neg A\seq}{%
\infer[\neg\text{-g}]{\onslide<5->{B,}A,B,\neg A\seq}{%
\infer[\text{Axiome}]{\onslide<5->{B,}A,B\seq A}{}}}}}}$$
\onslide<6->

On a prouv\'e $B\imp\bottom$, on ajoute la r\`egle
$$B~\ra~\only<6>{B\wedge}\bottom$$ 

\end{frame}

\begin{frame}[label=current]
  \frametitle{Notre Approche par l'Exemple (suite)}
Paradoxe de Russell: $R\in R~\ra~\forall y.~y\sim R\imp y\in R \imp C$
o\`u $y\sim z~\df~\forall x.~(y\in x\imp z\in x)$
\pause

{\tiny
$$\infer[\text{Coup}]{\seq \onslide<4->{C}}{%
\infer[\uparrow\text{-d}]{\seq R\in R\onslide<4->{,C}}{%
\infer[\forall\text{-d}]{\seq R\in R,\forall y.~y\sim R\imp y\in R\imp C\onslide<4->{,C}}{%
\infer[\imp\text{-d}]{\seq R\in R,c_0\sim R\imp c_0\in R\imp C\onslide<4->{,C}}{%
\infer[\imp\text{-d}]{c_0\sim R\seq R\in R,c_0\in R\imp C\onslide<4->{,C}}{%
\infer[\forall\text{-g}]{c_0\sim R,c_0\in R\seq R\in R,C}{%
\infer[\imp\text{-g}]{c_0\in t_0\imp R\in t_0,c_0\in R\seq R\in R, C}{%
R\in t_0,c_0\in R\seq R\in R, C & c_0\in R\seq c_0\in t_0,R\in R,
C}}}}}} &
%
\infer[\uparrow\text{-g}]{R\in R\seq \onslide<4->{C}}{%
\infer[\forall\text{-g}]{R\in R,\forall y.~y\sim R\imp y\in R\imp C\seq \onslide<4->{C}}{%
\infer[\imp\text{-g}]{R\in R,t_1\sim R\imp t_1\in R\imp C\seq \onslide<4->{C}}{%
\infer[\imp\text{-g}]{R\in R,t_1\in R\imp C\seq \onslide<4->{C}}{%
\alert<4>{R\in R,C\seq \onslide<4->{C}}& R\in R\seq t_1\in R\onslide<4->{,C}} &
\infer[\forall\text{-d}]{R\in R\seq t_1\sim R\onslide<4->{, C}}{%
\infer[\imp\text{-d}]{R\in R\seq t_1\in c_1\imp R\in c_1\onslide<4->{, C}}{%
R\in R, t_1\in c_1\seq R\in c_1\onslide<4->{, C}}}}}}}$$
}
\onslide<3->

Unification (sur les $t_i$): $t_0 = R, t_1 = R$

\onslide<5->
Nouvelle r\`egle: $$C~\ra~\top$$
\end{frame}

\subsection{Perspectives}
\begin{frame}
  \frametitle{Perspectives}

  \begin{itemize}[<+->]
    \item Possibilit\'e de traiter les th\'eories avec quantificateurs
    \item Pas besoin de mod\`ele $\imp$ appliquable aux th\'eories
    inconsistantes 
  \end{itemize}
 
\onslide<3->{mais \ldots}

  \begin{itemize}
    \item<3-> 3 propositions atomiques ou plus dans la preuve avec coupure
    ? 0 ?
    \item<4-> Complexit\'e ? 
  \end{itemize}

\onslide<5->{Il reste \`a:}
\begin{itemize}
\item<5-> trouver un ordre convenable pour que les preuves
critiques correspondent \`a celle d\'ecrites
\item<6-> bien d\'efinir la relation entre r\`egle de r\'e\'ecriture sur les
propositions et conclusion d'une preuve
\end{itemize}

\end{frame}

\bibliographystyle{../aacs/fr-apalike}
\bibliography{../aacs/abbrev,../aacs/aacs,../aacs/protheo}

\nologo
\begin{frame}[label=CS]
\begin{beamerboxesrounded}[shadow=true]{\textbf{Règles d'Inférence de
      la Complétion Standard} \cite{KnuthBendix70,Bachmair-87}}
\begin{center}
\begin{tabular}{@{}p{.5\textwidth}@{}p{.5\textwidth}@{}}
\Rule{Déduit:}
Si $s=t\in CP(R)$
$$E,R~~\infers~~ E\cup\{s=t\},R$$
&
\Rule{Oriente:}
Si $s\tg t$
$$ E\cup\{s=t\},R~~\infers~~ E, R\cup\{s\rightarrow t\}$$
\\
\Rule{Supprime:}
$$E\cup\{s=s\},R~~\infers~~ E,R$$
&
\Rule{Simplifie:}
Si $s\rewrite[R] u$
$$ E\cup\{s=t\},R~~\infers~~ E\cup\{u=t\}, R$$
\\
\Rule{Compose:}
Si $t\rewrite[R] u$
$$E,R\cup\{s\rightarrow t\}~~\infers~~ E,R\cup\{s\rightarrow u\}$$
&
\Rule{Combine:}
Si $\rpfstep s{v\rightarrow w\in R}{}u$, et $s\encord
v$,
$$ E,R\cup\{s\rightarrow t\}~~\infers~~ E\cup\{u=t\}, R$$
\end{tabular}
\end{center}
\end{beamerboxesrounded}

\hyperlink{p_KB}{\beamerreturnbutton{Retour}}
\end{frame}

\end{document}
