\documentclass[notes=none,mathserif]{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{/Users/gburel/asbi/aacs/macros_modified}
\input{sequents}


\newcommand{\yeslogo}{\logo{\includegraphics[height=.07\textheight]{loria.jpg}\hspace{.04\textheight}\includegraphics[height=.07\textheight]{logo_uhp.jpg}}}
\newcommand{\nologo}{\logo{}}

\title[Systèmes de
  preuves ordonnées]{Étude et instances de syst\`emes de preuves ordonn\'ees} 
\subtitle{École Jeunes Chercheurs en Programmation}
\author{Guillaume Burel}
\date{juin 2006}
\institute[LORIA/UHP]{LORIA -- Université Henri Poincaré\\Encadrant : Claude Kirchner}
\setbeamertemplate{caption}[numbered]
\logo{\includegraphics[height=.15\textheight]{loria.jpg}\hspace{.08\textheight}\includegraphics[height=.15\textheight]{logo_uhp.jpg}}

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

\begin{frame}
  \frametitle{Introduction}

Démonstration automatique et interactive: de nombreux formalismes
logiques : \alert<3>{séquents}, \alert<4>{preuves équationnelles}, \alert<5>{formes clausales}\ldots\pause
\smallskip

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<4>{ (en «vallée»)}\pause,
preuves qui appliquent la résolution sur les grands atomes en premier
\medskip\pause

Cadre des systèmes canoniques abstraits (SCA) introduit par
N.Dershowitz et C. Kirchner: la
notion de bonne preuve est traduite par un \alert<6>{ordre sur les
  preuves}
\pause\smallskip

Notion de complétion abstraite qui permet de retrouver un système
ayant les bonnes propriétés; ici on va l'appliquer à la déduction
modulo pour recouvrer l'élimination des coupures

\end{frame}



\begin{frame}<9>
\frametitle{Définitions}
\only<1>{\input{../presentation/pres_1.pdf_t}}
\only<2>{\input{../presentation/pres_2.pdf_t}}
\only<3>{\input{../presentation/pres_3.pdf_t}}
\only<4>{\input{../presentation/pres_4.pdf_t}}
\only<5>{\input{../presentation/pres_first.pdf_t}}
\only<6>{\input{../presentation/pres_proof.pdf_t}}
\only<7>{\input{../presentation/pres_order.pdf_t}}
\only<8->{\input{../presentation/pres_final.pdf_t}}

\onslide<9>{+ 5 postulats\\
$\Th A~\df~\Cl{\Pf A}$}

\end{frame}

\nologo
\begin{frame}
\frametitle{Complétion}
\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}
\pause

La complétion consiste à ajouter les conclusions des preuves
critiques:
$$A\leadsto A\cup\{\Cl p\st p\text{ critique}\}$$\pause
\begin{ftheo}[Complétude]
La limite $A_\infty$ de cette procédure est complète:

$$\Th{A_0}\subseteq\Cl{\Pf{A_\infty}\cap\mu\Pf{\Th A_0}}$$
\end{ftheo}
\end{frame}

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

Déduction modulo = déduction + calcul (principe de Poincaré)\pause
\medskip

Déduction: calcul des séquents de Gentzen
\begin{columns}
\column{.5\textwidth}
$$\Axiomm\Gamma\Delta A A$$
$$\Notd\Gamma\Delta A A$$
$$\Andd\Gamma\Delta {A\wedge B} A B$$
$$\Exd\Gamma\Delta{\exists x.~A} A t x$$

\column{.5\textwidth}
$$\Cut\Gamma\Delta A A$$
$$\Impd\Gamma\Delta {A\imp B}A B$$
$$\Ord\Gamma\Delta {A\vee B}A B$$
$$\Alld\Gamma\Delta{\forall x.~A}A c x\text{ avec $c$ fraîche}$$
\end{columns}

\pause\medskip
 
Calcul: règles de conversion
$$\Convg\Gamma\Delta A B \quad\text{ si }A\equiv B\quad\Convd\Gamma\Delta A B$$


\end{frame}

\begin{frame}
  \frametitle{Preuve critique en déduction modulo}
Congruence (Crabbé): $ A\limp B\wedge \neg A$

\begin{overlayarea}{\textwidth}{3cm}
\only<1>{\vspace{1cm}}%
 $$\infer[\text{Coup}]{\alert<6>{\onslide<5->{B}\seq}}{%
\infer[\uparrow\text{-g}]{\onslide<5->{B,}A\seq}{%
\only<1>{A,B\wedge\neg A\seq}%
\only<2->{\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}{}}}}}
%
&
%
\infer[\uparrow\text{-d}]{\onslide<5->{B}\seq A}{%
\only<1-2>{\seq B\wedge\neg A,A}%
\only<3->{\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}{}}}}} }$$
\end{overlayarea}
\onslide<6->
Il n'y a pas de preuve sans coupure de $B\seq$ 
\onslide<7->

On a prouv\'e $B\imp\bot$, on ajoute la r\`egle
$$B~\ra~\only<7>{B\wedge}\bot$$ 
\onslide<8->
Avec cette règle ajoutée, le système a la propriété d'élimination des coupures

\end{frame}

%% \yeslogo
%% \begin{frame}
%%   \frametitle{Extension avec des quantificateurs}
%%   Congruence: $ A\limp (\exists x.~B\wedge P(x))\wedge \neg A$

%%  $$\footnotesize\infer[\text{Coup}]{(\exists x.~B\wedge P(x))\seq}{%
%% \infer[\uparrow\text{-d}]{(\exists x.~B\wedge P(x))\seq A}{%
%% \infer*{(\exists x.~B\wedge P(x))\seq (\exists x.~B\wedge P(x))\wedge\neg A,A}{}
%% }&
%% \infer[\uparrow\text{-g}]{(\exists x.~B\wedge P(x)),A\seq}{
%% \infer*{(\exists x.~B\wedge P(x)),A,(\exists x.~B\wedge
%%   P(x))\wedge\neg A\seq}{}
%% }}$$
%% \pause

%% On doit transformer $(\exists x.~B\wedge P(x))\seq$ en règle de
%% réécriture sur les propositions (on ne peut réécrire que des formules atomiques):
%% $$\only<2>{(\exists x.~B\wedge P(x))\seq}%
%% \only<3>{B\wedge P(y)\seq}%
%% \only<4>{B\seq\neg P(y)}%
%% \only<5>{B\rightarrow B\wedge\forall y.~\neg P(y)}$$

%% \end{frame}

%% \begin{frame}
%%   \frametitle{Limitations}

%% Comment faire pour transformer le séquent $\forall x.~P(x)\seq\exists
%% y.~P(y)$ ? 
%% \bigskip\pause

%% On peut penser à utiliser l'inférence profonde, puisque les règles
%% d'inférence y sont assimilables à des règles de réécriture sur les
%% propositions
%% \medskip\pause

%% Exemple de preuve (supposée) critique pour Crabbé:

%% $$\infer[i\uparrow]{\text{f}}{
%% \infer[c\downarrow]{(a,\overline a)}{
%% \infer[conv]{(a,[\overline a,\overline a])}{
%% \infer[i\downarrow]{(a,[\overline a,\overline b,a])}{
%% \infer[c\downarrow]{a}{
%% \infer[conv]{[a,a]}{
%% \infer[s]{[a,(b,\overline a)]}{
%% \infer[i\downarrow]{(b,[a,\overline a])}{b}}}}}}}}\text{
%%         correspondrait à une règle   }b\rightarrow \text{f}$$
%% \end{frame}

\begin{frame}
  \frametitle{Perspectives}

  \begin{itemize}[<+->]
  \item Les quantificateurs posent problème dans certains cas
    $\rightarrow$ étude par exemple de l'inférence profonde comme
    système canonique abstrait, de fa\c con à obtenir un algorithme de
    complétion donnant la propriété d'élimination des coupures pour
    toute formule du premier ordre

  \item Implémentation (à l'aide d'une variante de la méthode des
    tableaux pour la déduction modulo) $\rightarrow$ TOM, OCaml/Zenon ?

  \item Étude d'autres systèmes de preuves, par exemple ceux qui \'evoluent avec
    la th\'eorie, comme la d\'eduction surnaturelle
    introduite par B. Wack, éventuellement modification des systèmes
    canoniques abstraits pour couvrir ces cas
    
  \end{itemize}

\end{frame}


\bibliographystyle{apalike}
\bibliography{/Users/gburel/asbi/aacs/abbrev,/Users/gburel/asbi/dedmod/aacs,/Users/gburel/asbi/aacs/protheo}

\end{document}
