\documentclass[ignorenonframetext,mathserif,notheorems]{beamer}
\usepackage[latin1]{inputenc}
%\usepackage{pslatex}
%\usepackage[french]{babel}
\mode<presentation>{\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_en}

%\includeonlyframes{current}

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

\title[Completion for Cut Elimination]{An Abstract Completion Procedure for Cut Elimination in Deduction Modulo} 
\subtitle{LICS 2006}
\author[Burel \& Kirchner]{Guillaume Burel + Claude Kirchner}
\date{Tuesday, August 15th, 2006}
\institute[LORIA -- Nancy]{LORIA $\times$ (École
  Normale Supérieure de Lyon + INRIA)}
\setbeamertemplate{caption}[numbered]
\logo{\includegraphics[height=.15\textheight]{loria.jpg}}

\begin{document}

\mode<article>{\maketitle}
\mode<presentation>{\frame{\titlepage}}
\mode<presentation>{\logo{\includegraphics[height=.07\textheight]{loria.jpg}}}

\section{Deduction Modulo}
\begin{frame}
\frametitle{Sequent Calculus Modulo}

Deduction modulo = deduction + calculus (Poincaré's Principle)\pause
\medskip

Deduction: Gentzen's sequent calculus
%% \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{ with $c$ fresh}$$
%% \end{columns}

\pause\medskip
 
Calculus: conversion rules
\begin{overprint}
\onslide<3| handout:0>$$\Convg\Gamma\Delta A B \quad\text{ if }A\equiv
  B\quad\Convd\Gamma\Delta A B$$
\onslide<4->$$\Upg\Gamma\Delta A B \quad\text{ if }A\ra
  B\quad\Upd\Gamma\Delta A B$$
\end{overprint}
\onslide<4->{Here: rewriting atomic propositions to propositions}

\end{frame}

\begin{frame}[label=current]
\frametitle{Cut Elimination Property ?}
Can we prove every valid sequent without the cut rule ?
\medskip

\begin{overlayarea}{\textwidth}{.6\textheight}
\only<8-| handout:2>{No\mode<article>{:}\medskip

}
\only<2-7| handout:1>{
A critical proof is a minimal counter-example of the required property (here, the cut elimination)
 
Congruence~\cite{Crabbe}: $ A\limp B\wedge \neg A$

\begin{overlayarea}{\textwidth}{3cm}
\only<2| handout:0| article:0>{\vspace{1cm}}%
 $$\infer[\text{Cut}]{\alert<7>{\onslide<6->{B}\seq}}{%
\infer[\uparrow\text{-l}]{\onslide<6->{B,}A\seq}{%
\only<2| handout:0| article:0>{A,B\wedge\neg A\seq}%
\only<3->{\infer[\wedge\text{-l}]{\onslide<6->{B,}A,B\wedge\neg A\seq}{%
\infer[\neg\text{-l}]{\onslide<6->{B,}A,B,\neg A\seq}{%
\infer[\text{Axiom}]{\onslide<6->{B,}A,B\seq A}{}}}}}
%
&
%
\infer[\uparrow\text{-r}]{\onslide<6->{B}\seq A}{%
\only<2-3| handout:0| article:0>{\seq B\wedge\neg A,A}%
\only<4->{\infer[\wedge\text{-r}]{\onslide<6->{B}\seq B\wedge\neg A,A}{%
{\onslide<5->{\alert<5>B}\seq B,A}%
& 
\infer[\neg\text{-r}]{\onslide<6->{B}\seq \neg A,A}{%
\infer[\text{Axiom}]{\onslide<6->{B,}A\seq A}{}}}}} }$$
\end{overlayarea}
\onslide<7->
There is \alert<7>{no} cut-free proof of $B\seq$ (no inference rules to be applied)}

\only<8-| handout:2>{\onslide<9->\mode<article>{\bigskip

}%
How can we overcome this ?\onslide<10->\medskip

We could complete our system by adding a new rule $B \rightarrow \bot$
\onslide<11->\medskip

How can we formalize this ?\onslide<12->\medskip

Using the Abstract Canonical Systems framework \cite{acp}: 
proof ordering $\Rightarrow$ critical proofs $\Rightarrow$ abstract completion procedure $\Rightarrow$ completeness result
}
\end{overlayarea}

\end{frame}

%% \section{Abstract Completion through Critical Proofs}
%% \begin{frame}
%% \frametitle{Abstract Completion}

%% \begin{definition}[Critical Proof]\label{defi:critical}
%%   $p\in\mu\Pfa A$ is \emph{critical} if:
%%     $$p\not\in\mu\Pf{Th A}~~\wedge~~\forall q\lhd p.~q\in\mu\Pf{\Th A}$$
%% \end{definition}
%%   i.e. $p$ is one of the smallest proofs that do not have the required
%%   property (not minimal for all presentations of the theory)\pause\medskip

%% In deduction modulo:

%% $$\infer[\text{Cut}]{\Gamma\seq\Delta}{%
%% \infer[\uparrow\text{-l}]{\Gamma,A\seq\Delta}{%
%% \infer*{\Gamma,A,P\seq\Delta}{}} &
%% \infer[\uparrow\text{-r}]{\Gamma\seq A,\Delta}{%
%% \infer*{\Gamma\seq A,Q,\Delta}{}}}$$
%% if $A\ra P$ and $A\ra Q$

%% \end{frame}

%% \begin{frame}
%% \frametitle{Completion procedure}
%% To complete the system, we have to add the conclusions of the critical proofs:
%% $$A\leadsto A\cup\{\Cl p\st p\text{ critical}\}$$\pause
%% \begin{theorem}[Completeness]
%% The limit $A_\infty$ of this completion procedure can be used to build
%% the minimal proofs in all presentations:
%% $$\Th{A_0}\subseteq\Cl{\Pf{A_\infty}\cap\mu\Pf{\Th A_0}}$$
%% \end{theorem}
%% \end{frame}

\section{Conclusion}
\begin{frame}
\frametitle{Issues and Perspectives}
\textbf{Theorem:} Deduction modulo is an instance of Abstract Canonical System
\pause\medskip

but\ldots
\begin{itemize}[<+->]
\item undecidability results (cut elimination, search of critical proof)
\item needs some restriction on quantifiers
\end{itemize}
\medskip

\begin{itemize}[<+->]
\item extends this to the whole first-order logic
\item implementation (ML or TOM or Coq ?)
\end{itemize}
\medskip

\onslide<1->
\large
\url{{http://www.loria.fr/\~ burel/download/gencomp.pdf}}
\end{frame}

\frame<0>{\mode<presentation>{\frametitle{Bibliography}}
\bibliographystyle{apalike}
\bibliography{../../asbi/dedmod/aacs.bib}}

\end{document}

