\documentclass[12pt]{beamer}
\usepackage[latin9]{inputenc}
\usepackage{logictheme}
\usefonttheme[onlymath]{serif}

\usecolortheme[rgb={.02,.3,.05}]{structure}
\setbeamercolor{palette secondary}{fg=black!60!averagebackgroundcolor}

\setbeamertemplate{theorems}[ams style]
%\setbeamercolor{titlelike} 
%	       {use={palette primary},fg=black,bg=palette
%		 primary.bg} 

\input{/Users/gburel/asbi/aacs/macros_modified}
\input{entete}
\usepackage{prooftree}
\input{seqcalmod}


\providecommand{\vect}[2][n]{{#2}_1,\ldots,{#2}_{#1}}

\title{Cut Elimination in Deduction Modulo by 
Abstract Completion}
\subtitle[LFCS'07]{Symposium on Logical Foundations of Computer Science}
\author[Guillaume Burel \and Claude Kirchner]{\underline{Guillaume Burel}\inst{1,3} \and Claude Kirchner\inst{2,3}}
\date[2007-06-05]{June 5$^{\text{th}}$, 2007}
\institute[(UHP+INRIA)\times LORIA]{\hfill\inst{1}Université Henri Poincaré\hfill\inst{2}INRIA\hfill\inst{3}LORIA\hfill~}
\setbeamertemplate{caption}[numbered]
\logo{\includegraphics[height=.06\textheight]{logo_uhp.jpg}\hspace{.04\textheight}\includegraphics[height=.06\textheight]{logo-inria.png}\hspace{.04\textheight}\includegraphics[height=.06\textheight]{loria.jpg}}

%\includeonlyframes{current}

\newcommand\lvdash[2][]{\mathrel{\rule{.4pt}{1.5ex}\kern-.14em\lower-.1em\hbox{$\frac{\scriptstyle~#1\,}{\scriptstyle~#2\,}$}}}
\newcommand\Hvdash[2][]{\mathrel{\textup{H}\kern-.25em\lower-.105em\hbox{$\frac{~#1\,}{~#2\,}$}}}
\newcommand\Nvdash[2][]{\mathrel{\textup{N}\kern-.25em\lower-.105em\hbox{$\frac{~#1\,}{~#2\,}$}}}
  
\begin{document}


\begin{frame}
\titlepage
\end{frame}

\section{Introduction}
\subsection{Deduction modulo}
 
\begin{frame}
  \frametitle{A simple proof?}
\onslide<3->{$\Gamma= \alert<4>{\forall x~y.~s(x)+y =
    x+s(y)},~\alert<5>{\forall x.~0+x=x}\onslide<6->{,\alert<6>{~\forall
    x~y~z.~x=y\imp y=z\imp x=z}}$}

\relsize{-1}
  \begin{prooftree}
\[\[\[
\[
\[\Axiomm<8->\onslide<7->{1+1=2\vdash 1+1=2}\]
\[\Axiomm<8->\onslide<7->{0+2=2\vdash 0+2=2}\]
\ImpL<7->
\shiftleft40pt \onslide<7->{\begin{array}{r}\Gamma,0+2=2\\
   0+2=2\imp 1+1=2
  \end{array}\vdash 1+1=2}
\]\kern-70pt
\[\Axiomm<8->\onslide<7->{1+1=0+2\vdash 1+1=0+2}\]
\ImpL<7->
\shiftleft40pt \onslide<6->{\begin{array}{r}\Gamma,1+1=0+2,0+2=2\\
    1+1=0+2\imp 0+2=2\imp 1+1=2
  \end{array}\vdash 1+1=2}\]
\AllL<6->[
  \begin{array}{l}
    x:=1+1\\y:=0+2\\z:=2
  \end{array}
]
\onslide<5->{\Gamma,1+1=0+2,0+2=2\vdash 1+1=2}\]
\AllL<5->[x:=2]
\onslide<4->{\Gamma,1+1=0+2\vdash 1+1=2}
\]
\AllL<4->[x:=0,y:=s(0)]
\onslide<3->{\Gamma}\vdash\alt<1,3->{1+1=2}{s(0)+s(0)=s(s(0))}
\end{prooftree}

\end{frame}

\begin{frame}
\frametitle{Proving vs. verifying}
  Poincaré 1902:

  ``Ce n'est pas une démonstration proprement dite [\ldots] c'est une
  vérification''
\medskip\pause

Poincaré's principle: identifying computation and deduction

$\leadsto$ deduction modulo \cite{DHK-TPM-JAR}
\end{frame}

\begin{frame}
  \frametitle{Deduction modulo}

Computational part expressed as a rewrite system over terms and
propositions
\pause

For instance $$
\begin{array}{c}
  s(x)+ y\rightarrow  x + s(y)\\
  x\times y = 0\rightarrow x=0\vee y=0
\end{array}$$
\pause

Inferences performed modulo this congruence:

$$\begin{prooftree}
\Gamma,\subst Pyx\vdash\Delta
\ExL[~~~Q\sRew^*\exists x.~P\text{, $y$ fresh}]
\Gamma,Q\vdash\Delta
\end{prooftree}
$$

\end{frame}

\begin{frame}
\frametitle{Example of a proof in deduction modulo}
\begin{prooftree}
\TopR[1+1=2\rewrite^*2=2\rewrite\top]
\vdash 1+1=2
\end{prooftree}
\bigskip\pause

\relsize{-1}
\begin{prooftree}
\[%1
\[%2
\[\Axiomm<5->[
  \begin{array}{l}
    z-2=0\\\sRew^*z=2
  \end{array}
]
\onslide<4->{z-2=0\vdash z=2}\]
\kern-30pt\[\Axiomm<5->[ \begin{array}{l}z-2=0\\\sRew^*z=2
  \end{array}
]
\lower-3em\hbox{\onslide<4->{$z-2=0\vdash z=2$}}\kern-10pt\lower-.75em\hbox{\onslide<4->{$\vdots$}}\hspace{10pt}\]
\OrL<3->[ \begin{array}{l}z\times z- 4 z + 4 = 0\\\sRew^* (z-2)\times(z-2) =
    0\\\sRew^* z-2=0\vee z-2 =
    0
  \end{array}
]
z\times z- 4 z + 4 = 0\vdash z=2
\]%2
\ImpR
\vdash z\times z- 4 z + 4 = 0 \imp z=2\]%1
\AllR[z\text{ is fresh}]
\vdash\forall x.~x\times x- 4 x + 4 = 0 \imp x=2
\end{prooftree}
  
\end{frame}

\begin{frame}
\frametitle{Asymmetric sequent calculus modulo}

\cite{gentzen:untersuchungen} sequent calculus:
\medskip

\begin{prooftree}
\Gamma, A\vdash\Delta~~~~~
\Gamma\vdash A,\Delta
\Cut
\Gamma\vdash\Delta 
\end{prooftree}\hfill
\begin{prooftree}
\Gamma,\subst Pyx\vdash \Delta
\ExL[y\text{ fresh}]
\Gamma,\exists x.~P\vdash\Delta
\end{prooftree}
\medskip

\begin{prooftree}
\Gamma, B\vdash\Delta~~~~~
\Gamma\vdash A,\Delta
\ImpL
\Gamma, A\imp B\vdash\Delta 
\end{prooftree}\hfill
\begin{prooftree}
\Gamma\vdash \subst Ptx,\exists x.~P,\Delta
\ExR
\Gamma\vdash \exists x.~P,\Delta
\end{prooftree}

\bigskip

+ externalized congruence rules:
\medskip

\begin{prooftree}
\Gamma, A,P\vdash\Delta
\UpL[\text{if }A\rewrite P]
\Gamma, A\vdash\Delta 
\end{prooftree}\hfill
\begin{prooftree}
\Gamma\vdash A,P,\Delta
\UpR[\text{if }A\rewrite P]
\Gamma\vdash A,\Delta 
\end{prooftree}

\end{frame}

\begin{frame}
\frametitle{Important facts about deduction modulo}
Simulates theories:
\begin{itemize}
\item Higher Order Logic \cite{hollambdasigma}
\item Zermelo [Dowek and Miquel, 2007]
\item Arithmetic \cite{arith}
\item Pure Type Systems \cite{CousineauDowek}
\end{itemize}
\medskip

Proof search methods:
\begin{itemize}
\item Resolution: ENAR \cite{DHK-TPM-JAR}
\item Tableaux: TaMed \cite{Bonichon04}
\end{itemize}
\medskip

Proof-length speed-ups \cite{burel07csl}
\end{frame}

\subsection{Cut admissibility}
\begin{frame}
  \frametitle{Deduction modulo and cut admissibility}
  \begin{definition}
    A rewrite systems R \emph{admits} Cut if all sequents provable
    modulo R can be
    proved modulo R without Cut
  \end{definition}
\bigskip

$\emptyset$ admits Cut (Gentzen's Hauptsatz)

Cut admissibility implies 
\begin{itemize}
\item subformula property
\item completeness of automated provers
\end{itemize}



Do all rewrite systems admit Cut ?
\end{frame}

\begin{frame}[label=current]
\frametitle{Crabbé counterexample}
Rewrite system: $A\rightarrow B\wedge\neg A$
\medskip\pause

Search for a minimal counterexample:

\relsize{-1}
\begin{prooftree}
\[%1  
\[%2
\[%3
\[%4
\[%5
\Axiomm<3->
\onslide<5->{B,}\onslide<3->{A,B,B\vdash A}
\]%5
\NotL<3->
\onslide<5->{B,}\onslide<3->{A,B,\neg A,B\vdash}
\]%4
\AndL<3->
\onslide<5->{B,}\onslide<3->{A,B\wedge\neg A,B\vdash}
\]%3
\UpL<3->
\onslide<5->{B,}\onslide<3->{A,B\vdash}
\]%2
\AndL<3->
\onslide<5->{B,}A\wedge B\vdash
\]%1
\[%1  
\[%2
\[%3
\[%4
\Axiomm<5->
\onslide<5->{B}\onslide<4->{\vdash A,B}
\]%4
\[%4
\[%5
\Axiomm<4->
\onslide<5->{B,}\onslide<4->{A\vdash A}
\]%5
\NotR<4->
\onslide<5->{B}\onslide<4->{\vdash A,\neg A}
\]%4
\AndR<4->
\onslide<5->{B}\onslide<4->{\vdash A,B\wedge\neg A}
\]%3
\UpR<4->
\onslide<5->{B}\onslide<4->{\vdash A}
\]%2
\[%2
\Axiomm<5->
\onslide<5->{B}\onslide<4->{\vdash B}
\]%2
\AndR<4->
\onslide<5->{B}\vdash A\wedge B
\]%1
\Cut
\onslide<5->{B}\vdash
\end{prooftree}
  
\end{frame}


\begin{frame}
\frametitle{Cut elimination}

If there is no modulo, Cut is admissible (Gentzen's Hauptsatz)

There exists a cut elimination procedure:

\begin{center}
  \begin{prooftree}
    \[
    \Gamma, A, B\vdash \Delta
    \AndL
    \Gamma, A\wedge B\vdash \Delta
    \]
    \[
    \Gamma\vdash A,\Delta~~~~
    \Gamma\vdash B,\Delta~~~~
    \AndL
    \Gamma\vdash A\wedge B,\Delta
    \]
    \Cut
    \Gamma\vdash\Delta
  \end{prooftree}
\end{center}
becomes
\begin{center}
  \begin{prooftree}
    \[
    \Gamma, A, B\vdash \Delta~~~~\Gamma, A\vdash B,\Delta
    \Cut
    \Gamma, A\vdash \Delta
    \]
    \Gamma\vdash A,\Delta\Cut
    \Gamma\vdash\Delta 
  \end{prooftree}
\end{center}
Proofs with cuts are replaced by smaller counterexamples
\end{frame}

\begin{frame}
  \frametitle{Crabbé's counterexample (Cont.)}

$A\rightarrow B\wedge\neg A$
\bigskip

\relsize{-1}
\alt<1>{\begin{prooftree}
\[%0
\[%1
\[%2
\[%3
\[%4
\Axiomm
B,A,B,B\vdash A
\]%4
\NotL
B,A,B,\neg A,B\vdash
\]%3
\AndL
B,A,B\wedge\neg A,B\vdash
\]%2
\UpL
B,A,B\vdash
\]%1
\[%1
\Axiomm
B,A\vdash B
\]%1
\Cut
B,A\vdash
\]%0
%\kern-30pt
\[%1
\[%2
\[%3
\Axiomm
B\vdash B,A
\]%3
\[%3
\[%4
\Axiomm
B,A\vdash A
\]%4
\NotR
B\vdash\neg A,A
\]%3
\AndR
B\vdash B\wedge\neg A,A
\]%2
\UpR
%\lower-2em\hbox{$
B\vdash A
%$}\kern-10pt\lower-.25em\hbox{$\vdots$}\hspace{10pt}
\]%1
\Cut
B\vdash
  \end{prooftree}}{%
\begin{prooftree}
\[%1
\[%2
\[%3
\[%4
\Axiomm
B,A,B\vdash A
\]%4
\NotL
B,A,B,\neg A\vdash
\]%3
\AndL
B,A,B\wedge\neg A\vdash
\]%2
\UpL<2-| alert@3>
B,\alert<3->{A}\vdash
\]%1
\[%1
\[%2
\[%3
\Axiomm
B\vdash B,A
\]%3
\[%3
\[%4
\Axiomm
B,A\vdash A
\]%4
\NotR
B\vdash\neg A,A
\]%3
\AndR
B\vdash B\wedge\neg A,A
\]%2
\UpR<2-| alert@3>
B\vdash \alert<3>{A}
\]%1
\Cut<2-| alert@3>
B\vdash
  \end{prooftree}}
\bigskip

\relsize{1}
\onslide<3->
= minimal counterexample
\end{frame}

\begin{frame}
  \frametitle{Regaining Cut admissibility}

Need to build a proof of $B\vdash$
\medskip

Add a new rule to your system: $B\rightarrow \bot$
\medskip

\begin{center}
  \begin{prooftree}
    \[ 
    \BotL
    \bot\vdash
    \]
    \UpL
    B\vdash
  \end{prooftree}
\end{center}
\medskip

$\left\{
\begin{array}{l}
  A\rightarrow B\wedge\neg A\\
  B\rightarrow \bot
\end{array}\right.$ admits Cut
\end{frame}

\begin{frame}
  \frametitle{Term rewrite systems}

\cite{DBLP:conf/rta/Dowek03}: a \emph{term} rewrite system is
confluent iff it admits Cut
\bigskip

no longer true for \emph{proposition} rewrite systems (Crabbé)
\bigskip

If a TRS is not confluent, use standard (a.k.a. Knuth-Bendix)
completion to get an equivalent confluent TRS
\medskip

$\leadsto$ a generalized completion procedure to recover cut
admissibility ?
\end{frame}

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

\section{Limitations}
\begin{frame}
  \frametitle{Undecidability of cut admissibility}

  \begin{theorem}
The following problem is undecidable:

input: a rewrite system R

answer: determine if R admits Cut
  \end{theorem}
\pause

  \emph{Proof:}

Let $P$ be a first order proposition, $r,\in$ not in $P$,

let $R_P = \Big\{r\in r\rightarrow \forall y.~(\forall x.~y\in x\imp r\in
  x)\imp y\in r\imp P$
\medskip

$P$ is valid iff $R_P$ admits Cut

(Models for deduction modulo \cite{hermant-stpeter})

\end{frame}


\section{A Formalism for Abstract Completion}
\begin{frame}
  \frametitle{Abstract Canonical Systems \cite{acp}}
Based on proof ordering
\bigskip

General notion of canonicity, saturation, redundacy
\bigskip

Critical proofs = minimal counter-examples
\bigskip

Abstract definition of a completion procedure~\cite{aci}:

Adding the premises of proofs smaller than the critical ones
\end{frame}

\begin{frame}
  \frametitle{Proof ordering}
Proofs are trees:

Recursive Path Ordering
\bigskip

Precedence
\begin{itemize}
\item Proofs with Cut are greater: Cut$(P)>$ r
\item Compatible with the Cut elimination procedure: 

Cut$(P)>$ Cut$(Q)$ if $Q$ is a subformula of $P$
\end{itemize}


\end{frame}

\begin{frame}
  \frametitle{Critical Proofs}

  \begin{lemma}[Form of critical proofs]
    \begin{center}
      \begin{prooftree}
        \[\begin{array}{c}
        \pi_1\\
        \vdots\\
        \Gamma,A,P\vdash\Delta
        \end{array}
        \UpL[A\rewrite P]
        \Gamma,A\vdash\Delta
        \]
        \[\begin{array}{c}
        \pi_2\\\vdots\\
        \Gamma\vdash A,Q,\Delta
        \end{array}
        \UpR[A\rewrite Q]
        \Gamma\vdash A,\Delta\]
        \Cut
        \Gamma\vdash\Delta
      \end{prooftree}
    \end{center}
  \end{lemma}
  \bigskip\pause

Note: it is also undecidable to know if a sequent is the conclusion of
a critical proof or not
\end{frame}

\begin{frame}
  \frametitle{Smaller proofs}
Try to build a Cut-free proof:

\begin{itemize}
\item Indifferently apply any inference rule (apply $\forall$-l and
  $\exists$-r only once)

\item  When reaching a sequent $\Gamma,A\vdash\Delta$ with $A$ atomic, 

  rewrite $A$ into $A\wedge\forall \vect x.~(\neg\Gamma\vee\Delta)$

\item  $\leadsto$ the branch can be close

  (also symmetrically for $\Gamma\vdash A,\Delta$)
\end{itemize}
\bigskip

complete the rewrite system with these new $A\rightarrow
A\wedge\forall \vect x.~(\neg\Gamma\vee\Delta)$ and  $A\rightarrow
A\vee\exists \vect x.~(\Gamma\wedge\neg\Delta)$
\end{frame}

\begin{frame}
  \frametitle{Main theorem}
  \begin{theorem}
    Asymmetric deduction modulo is an instance of abstract canonical system
  \end{theorem}

\begin{corollary}[Cut Admissibility of the Limit]\label{theo:cutlim}
$\Gamma\vdash\Delta$ has a proof in $R_0$ if and only
if it has a \emph{cut-free} proof in $R_\infty$
\end{corollary}

\end{frame}





\section{Example of application}

\begin{frame}
  Crabbé with quantifiers: $A\rightarrow {(\exists x.~\forall
    y.~B\wedge P(x,y))\wedge \neg A}$ 

($Q(x)$ denotes $\forall
    y.~B\wedge P(x,y)$)

Critical proof:
\scriptsize
  \begin{prooftree}
\[%1
\[%2
\[%3
\[%4
\Axiomm
\exists x.~Q(x),A,\exists x.~Q(x)\vdash A
\]%4
\NotL
\exists x.~Q(x),A,\exists x.~Q(x),\neg A\vdash
\]%3
\AndL
\exists x.~Q(x),A,\exists x.~Q(x)\wedge\neg A\vdash
\]%2
\UpL
\exists x.~Q(x),A\vdash
\]%1
\[%1
\[%2
\[%3
\Axiomm
\exists x.~Q(x)\vdash \exists x.~Q(x),A
\]%3
\[%3
\[%4
\Axiomm
\exists x.~Q(x),A\vdash A
\]%4
\NotR
\exists x.~Q(x)\vdash\neg A,A
\]%3
\AndR
\exists x.~Q(x)\vdash \exists x.~Q(x)\wedge\neg A,A
\]%2
\UpR
\exists x.~Q(x)\vdash A
\]%1
\Cut
\exists x.~Q(x)\vdash
  \end{prooftree}
\end{frame}

\begin{frame}
Smaller proof:
\smaller
\begin{prooftree}
\[%1  
\[%2
\[%3
\[%4
\[%5
\[%6
\[%7
\[%8
\Axiomm<3->
\onslide<3->{Q(x),B,P(x,a)\vdash Q(x)}
\]%8
\NotL<3->
\onslide<3->{Q(x),B,\neg Q(x),P(x,a)\vdash}
\]%7
\[%7
\[%8
\Axiomm<3->
\onslide<3->{Q(x),B,P(x,a)\vdash P(x,a)}
\]%8
\NotL<3-> \onslide<3->{Q(x),B,\neg P(x,a),P(x,a)\vdash}
\]%7
\OrL<3->
\onslide<3->{Q(x),B,\neg Q(x)\vee\neg P(x,a),P(x,a)\vdash}
\]%6
\AllL<3->[z:=x]
\onslide<3->{Q(x),B,B,\forall z.~(\neg Q(z)\vee\neg P(z,a)),P(x,a)\vdash}
\]%5
\AndL<3->
\onslide<2->{Q(x),B,B\wedge\forall z.~(\neg Q(z)\vee\neg P(z,a)),P(x,a)\vdash}
\]%4
\UpL<2->
Q(x),B,P(x,a)\vdash
\]%3
\AndL
Q(x),B\wedge P(x,a)\vdash
\]%2
\AllL[y:=a]
Q(x)\vdash
\]%1
\ExL[x\text{ is fresh}]
  \exists x.~Q(x)\vdash
\end{prooftree}
\bigskip

\onslide<2->
New rule: $B\rightarrow B\wedge\forall z.~(\neg Q(z)\vee\neg P(z,a))$.
\end{frame}

\section{Conclusion}
\begin{frame}
  \begin{itemize}
  \item use of the ACS to define a procedure to recover Cut admissibility
    in Deduction Modulo
  \item boundaries of the approach through undecidability results
  \item description precise enough to be implemented (in Tom/ocaml\footnote{\url{http://tom.loria.fr/}})
  \end{itemize}
 \end{frame}

\begin{frame}
  \frametitle{Perspectives}

  \begin{itemize}
  \item too many critical proofs: refinement of the proof ordering
    (for instance $A\rightarrow A\vee\exists x.~P(x)$ subsumes
    $A\rightarrow A\vee P(t)$)
  \item provide cut admissibility but not normalization of proofs

  \item elimination of redundancies (simplification rules as in
    standard completion)

  \item link with superdeduction (new inference rules)

  \end{itemize}
\end{frame}

\bibliographystyle{apalike}
\bibliography{abbrev,burel,protheo,houtmann}







%% \appendix
%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% \newcommand{\M}{\mathcal M}
%% \begin{frame}
%%   \frametitle{Model for deduction modulo}
%% $\M$ is a model for $R$:

%% $\M$ is a model for the classical first order logic 

%% +
%% for all $P,Q$, $P\sRew^* Q$ is equivalent to $|P|_\M=|Q|_\M$

%% \begin{lemma}[\cite{hermant-stpeter}]
%% If there is a complete theory with Henkin witnesses $\Gamma$ with a
%% model $\M$ for $R$,

%% then $R$ admits Cut
%% \end{lemma}
%% \end{frame}

%% \begin{frame}
%%  \frametitle{Proof of the undecidability}

%% Reduction of the validity of first order logic

%% Let $P$ be a first order proposition, $r,\in$ not in $P$,

%% let $R = \Big\{r\in r\rightarrow \forall y.~(\forall x.~y\in x\imp r\in
%%   x)\imp y\in r\imp P$

%% $P$ is valid implies $P$ has a model, and this model is a model for
%%   $R$.

%% Reciprocally, if $P$ is not valid, there is no proof modulo $R$ of $\vdash P$ without
%% Cut

%% but there are proofs of $r\in r\vdash P$ and a proof of $\vdash r\in
%% r$ modulo $R$.
%% \end{frame}


%% \section{A completion procedure: informal approach}
%% \begin{frame}
%%   \frametitle{What is a completion procedure?}

%% some presentation (set of axioms) from which proofs can be build
%% {\usebeamercolor[fg]{palette primary}
%% for standard completion, some rewrite systems}

%% proofs having some good property 
%% {\usebeamercolor[fg]{palette primary}
%% valley proofs}

%%   \begin{itemize}
%%   \item find the smallest counterexamples
%% {\usebeamercolor[fg]{palette primary}
%% critical pairs
%% $c_1\longleftarrow\longrightarrow c_2$}
%% call them critical proofs

%% \item for each critical proof, find a proof which is closer to the
%%   required property
%% {\usebeamercolor[fg]{palette primary}
%% if $c_1>c_2$, this is
%% $c_1\longrightarrow c_2$}

%% \item complete your presentation by the assumptions needed to build
%%   the smaller proofs
%% {\usebeamercolor[fg]{palette primary}add $c_1\rightarrow c_2$ to the rewrite system}

%% \item repeat until you reach a fixpoint
%%   \end{itemize}
%% \end{frame}

%% \begin{frame}
%%   \frametitle{Critical proofs}
%% Property: Cut-free proofs

%%   \begin{itemize}
%%   \item with a Cut (counterexample)
%%   \item without too much Cuts (smallest counterexample)
%%   \item not too big (smallest counterexample)
%%   \end{itemize}
%% \pause

%% $\leadsto$ proofs with one Cut at the bottom
%% \begin{center}
%%   \begin{prooftree}
%%     \begin{array}{c}
%%       \pi_1\\\vdots\\
%%       \Gamma,A\vdash\Delta
%%     \end{array}~~~~\begin{array}{c}
%%       \pi_2\\\vdots\\
%%       \Gamma\vdash A,\Delta
%%     \end{array}
%%     \Cut
%%     \Gamma\vdash\Delta
%%   \end{prooftree}
%% \end{center}
%% \end{frame}


%% \begin{frame}
%%   \frametitle{Critical proofs}
%% Remaining case:

%% \begin{center}
%%   \begin{prooftree}
%%     \[\begin{array}{c}
%%     \pi_1\\
%%     \vdots\\
%%     \Gamma,A,P\vdash\Delta
%%     \end{array}
%%     \UpL[A\rewrite P]
%%     \Gamma,A\vdash\Delta
%%     \]
%%     \[\begin{array}{c}
%%     \pi_2\\\vdots\\
%%     \Gamma\vdash A,Q,\Delta
%%     \end{array}
%%     \UpR[A\rewrite Q]
%%     \Gamma\vdash A,\Delta\]
%%     \Cut
%%     \Gamma\vdash\Delta
%%   \end{prooftree}
%% \end{center}
%% \bigskip\pause

%% Note: it is also undecidable to know if a sequent is the conclusion of
%% a critical proof or not
%% \end{frame}


%% \begin{frame}
%%   \frametitle{Finding a smaller proof}
%% Try to build a Cut-free proof:

%% Indifferently apply any inference rule (apply $\forall$-l and
%% $\exists$-r only once)

%% When reaching a sequent $\Gamma,A\vdash\Delta$ with $A$ atomic, 
%% rewrite $A$ into $A\wedge\forall \vect x.~(\neg\Gamma\vee\Delta)$, so
%% that you can close the branch.

%% (also symmetrically for $\Gamma\vdash A,\Delta$)
%% \bigskip

%% complete the rewrite system with these new $A\rightarrow
%% A\wedge\forall \vect x.~(\neg\Gamma\vee\Delta)$ and  $A\rightarrow
%% A\vee\exists \vect x.~(\Gamma\wedge\neg\Delta)$

%% \end{frame}

%% \section{Formal approach: Abstract canonical systems}
%% \subsection{Definitions and postulates}
%% \begin{frame}
%% \frametitle{Definitions~\cite{acp}}
%% \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-> $\Th A = \Cl{\Pf A}$

%% \onslide<10-> subproof relation: $\rhd$
%% \end{frame}

%% \begin{frame}
%%   \frametitle{Postulates}
%%   \begin{itemize}
%%   \item     $A\subseteq\Th A$
%%   \item $\Th{\Th A} \subseteq \Th A$
%%   \item $a\in\Ax p \imp p\unrhd\triva a$
%%   \item $p\unrhd q\imp \Ax p\supseteq \Ax q$
%%   \item $p\rhd q > r \imp \exists v\in \Pfa{\Ax p\cup\Ax r}.~ p > v\rhd r$
%%   \end{itemize}
%% \end{frame}

%% \begin{frame}
%%   \frametitle{The completion procedure is completing}
%% Normal form: $\Nf{A} = \mu\Pf{\Th A}$ minimal proofs whatever the
%% presentation used

%% Critical proofs:
%% $\Crit A\df\left\{
%% \begin{array}{l}
%%   p\in\mu\Pf{A}\setminus\Nf{A}\st\\\forall q\in\Pf{A}.~p\rhd
%%   q\imp q\in\Nf{A}
%% \end{array}\right\}$

%% Completion procedure:
%% $A\leadsto A\cup \text{C}(A)$

%% where C$(A)$ contains proofs smaller than the critical ones

%%   \begin{theorem}[\cite{aci}]
%% This procedure is completing:
%% $$\Th A_0=\Cl{\Pf {A_\infty}\cap\Nf {A_0}}$$
%%   \end{theorem}
%% \end{frame}

%% \subsection{Deduction modulo is an instance}

%% \begin{frame}
%%   \frametitle{Instance}
%%   \begin{itemize}
%%   \item $\A$: rewrite systems
%%   \item $\P$: sequent calculus proofs modulo
%%   \item $\Ax p$: rewrite systems used in $p$
%%   \item $\Cl p$: rewrite system associated with the conclusion of $p$
%%     (rules used to build a cut-free proof of it)
%%   \item $>$: RPO with precedence
%%     $\text{Cut}(P)>\text{Cut}(Q)>\text{r}$ if $Q$ is a subformula of
%%     $P$
%%   \item $\rhd$: subproof modulo weakening
%%   \end{itemize}

%%   \begin{theorem}
%%     Asymmetric deduction modulo is an instance of abstract canonical system
%%   \end{theorem}
%% \end{frame}

%% \begin{frame}
%%   \frametitle{Consequence}
%% \begin{corollary}[Cut Admissibility of the Limit]\label{theo:cutlim}
%% $\Gamma\vdash\Delta$ has a proof in $R_0$ if and only
%% if it has a \emph{cut-free} proof in $R_\infty$
%% \end{corollary}

%% \end{frame}


\end{document}
