\documentclass{beamer}

\usepackage{proof}
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{url}
\usepackage{cmll}
%\usepackage{MnSymbol}
\usepackage{graphicx}
\usepackage{bussproofs}
%\usepackage[all]{xy}
\usepackage{comment}
\usepackage{lscape}

%\newcommand{\excl}{\mathrel{\rotatebox[origin=c]{180}{\ensuremath \multimap}}}

%\usepackage{txfonts}
%\usepackage{amsthm}

%\renewcommand{\labelenumi}{(\roman{enumi})}

\definecolor{dkblue}{rgb}{0,0,.7}
\definecolor{dkgreen}{rgb}{0,.5,0}
\definecolor{greyout}{rgb}{0.7,0.7,0.7}
%\newcommand\tc[2]{\textcolor{#1}{#2}}
%\newcommand\tcr[1]{\tc{darkred}{#1}}
\newcommand\tcg[1]{\tc{dkgreen}{#1}}
\newcommand\tcb[1]{\tc{dkblue}{#1}}
\newcommand\tcgy[1]{\tc{greyout}{#1}}
\newcommand\Tcr[1]{\tcr{\textbf{#1}}}
\newcommand\Tcg[1]{\tcg{\textbf{#1}}}
\newcommand\Tcb[1]{\tcb{\textbf{#1}}}

\newcommand{\tblue}[1]{\textcolor{blue}{#1}}
\newcommand{\tgreen}[1]{\textcolor{magenta}{#1}}
\newcommand{\tred}[1]{\textcolor{red}{#1}}
\newcommand{\TextRed}{\tred}

\def\parr{\oplus}
%\def\punit{\bot}
\def\punit{\mlze}
%\def\tunit{\mathrm{I}}
\def\tunit{\mltp}
%\def\sunit{\Phi}
\def\sunit{\cdot}
\def\limp{\multimap}
%\def\excl{\leftY}
\def\excl{{-\!\!\!<}}
\def\ltens{\otimes}
\def\merge{\bullet}

\def\seq{\Rightarrow}
%\def\seq{>}

\def\ll{\mathrm{LL}}
\def\mill{\mathrm{MILL}}
\def\mall{\mathrm{MALL}}
\def\mll{\mathrm{MLL}}
\def\fill{\mathrm{FILL}}
\def\biill{\mathrm{BiILL}}
\def\biilldc{\mathrm{BiILL}{\scriptstyle dc}}
%\def\fbills{\mathrm{BiILL}^{sn}}
\def\biillsn{\mathrm{BiILL}{\scriptstyle sn}}
%\def\fbilld{\mathrm{BiILL}^{dn}}
\def\biilldn{\mathrm{BiILL}{\scriptstyle dn}}
\def\filldc{\mathrm{FILL}{\scriptstyle dc}}
%\def\filld{\mathrm{FILL}^{dn}}
\def\filldn{\mathrm{FILL}{\scriptstyle dn}}
\def\impl{\supset}
\def\dimpl{\subset}
\def\bang{!}
\def\qm{?}

\def\drp{\mathit{drp}}
\def\rp{\mathit{rp}}

\newcommand{\binop}{\heartsuit}

\newcommand \seqtodisp[1]{\ulcorner{#1}\urcorner}
\newcommand\disptoseq[1]{\llcorner{#1}\lrcorner}
\def\Pc{\mathcal{P}}
\def\Qc{\mathcal{Q}}
\def\Sc{\mathcal{S}}
\def\Tc{\mathcal{T}}
\def\Uc{\mathcal{U}}
\def\Vc{\mathcal{V}}
\def\Xc{\mathcal{X}}
\def\Yc{\mathcal{Y}}
\def\Zc{\mathcal{Z}}

\def\turn{\vdash}
%\newcommand{\comment}[1]{}

\usepackage{color}
\definecolor{darkred}{cmyk}{0.0,1.0,1.0,0.3}
\newcommand\tc[2]{\textcolor{#1}{#2}}
\newcommand\tcr[1]{\tc{darkred}{#1}}

%%%%
%%%% Raj's defs. Need to be merged but want to chat with Ranald first
%%%%

%\def\fill{FILL}
%\def\ill{ILL}
%\def\mill{MILL}
\def\bill{BILL}
%\def\biill{BiILL}
\def\jill{JILL}
\def\gill{GILL}
\def\dill{DILL}

\def\gnab{?}
\def\adcn{\wedge}
\def\addn{\vee}
\def\adim{\to}
\def\adtp{\top}
\def\adbt{\bot}
%\def\mldn{\parr}
\def\mldn{\oplus}
\def\mlcn{\otimes}
\def\mltp{\mathbf{1}}
%\def\mltp{1}
\def\mlbt{\bot}
\def\mlze{\mathbf{0}}
%\def\mlze{0}
\def\mlim{\multimap}
\def\mlli{\multimap^{-1}}
\def\mlri{\multimap}
\def\mlrx{
       \mbox{\,\raisebox{0.14ex}{$\scriptstyle>$}\!\!\raisebox{0.14ex}{$\scriptstyle -$}\,}}
\def\mllx{\excl}
%\def\mllx{
%       \mbox{\,\raisebox{0.13ex}{$\scriptstyle-$}\!\!\raisebox{0.13ex}{$\scriptstyle <$}\,}}

\def\sequent{\vdash}

\newcommand{\imprightmc}{
 \AxiomC{$\Gamma, A \sequent B, \Delta$}
% \LeftLabel{$(\mlim R_1)$}
 \UnaryInfC{$\Gamma \sequent A \mlim B, \Delta$}
 \DisplayProof
}

\newcommand{\imprightsc}{
 \AxiomC{$\Gamma, A \sequent B$}
% \LeftLabel{$(\mlim R_1)$}
 \UnaryInfC{$\Gamma \sequent A \mlim B, \Delta$}
 \DisplayProof
}

\theoremstyle{plain}
\newtheorem{proposition}[theorem]{Proposition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\title{From Display Calculi to Decision Procedures for Full
  Intuitionistic Linear Logic}

\author{Ranald Clouston,
        Jeremy Dawson,
        \underline{Rajeev Gor\'e},
        Alwen Tiu}

\institute[ANU]{Logic and Computation Group\\
  Research School of Computer Science\\
  The Australian National University\\
  \url{rajeev.gore@anu.edu.au}}

\date{\today
\\[15px]
{\small
Published in Proc.\ 22nd EACSL Annual Conference 
\\ on Computer Science Logic, Turin September 2013 as
``Annotation-free sequent calculi for Full Intuitionistic Linear Logic''}
}

\begin{document}

\frame{\titlepage}

\begin{frame} \frametitle{Overview}

  \begin{description}[M]
  \item What is FILL?
  \item Existing sequent calculi
  \item A Display Calculus for FILL
  \item Nested Sequent Calculus for FILL
  \item Separation
  \item Decidability and Complexity
  \item Further Work
  \end{description}

\end{frame}

\begin{frame}
    \frametitle{Full Intuitionistic Linear Logic}

  \begin{description}[M]
  \item[$\ll$:] modal substructural logic without weakening and without
    contraction
    $\mlcn, \mldn, \mltp, \mlze,
    %\mlbt, 
    \mlim, \land, \lor, \adtp, \adbt, \bang, \gnab$ 
    \hfill Girard 1987
\vfill
  \item[$\mall$:] %linear logic without $\bang, \gnab$ i.e.
    $\mlcn, \mldn, \mltp, \mlze,
    %\mlbt, 
    \mlim, \land, \lor, \adtp, \adbt
    %, \bang, \gnab
    $
    \hfill drop exponentials
\vfill
  \item[$\mill$:] %linear logic without $\mldn, \mlze, \bang, \gnab$
    $\mlcn, \mltp, \mlim$
    \hfill intuitionistic
\vfill
  \item[$\mll$:]  $\mlcn, \mltp, \mlim, \mldn, \mlze$
    \hfill classical $((A \mlim \mlze) \mlim \mlze) \mlim A$
\vfill
  \item[$\fill$:]  $\mlcn, \mltp, \mlim, \mldn, \mlze$ \hfill
    Hyland and de Paiva 1993
 %  \item {\small 
 %   $
 %   (A \mlcn B) \mldn C) \mlim (A \mlcn (B \mldn C))
 %   \qquad
 %   ((A \mlim B) \mldn C) \mlim (A \mlim (B \mldn C))$
 %   }
 % \item weak-distribution \hfill Grishin(b)
  \end{description}

\end{frame}

\begin{frame}
  \frametitle{Categorial Semantics for $\fill$}

 \begin{description}[M]
    \item[$(\mlcn,\mltp,\mlim)$] is a symmetric monoidal closed structure 
    \item $A \mlcn B \mlim C$ 
          iff $A \mlim (B \mlim C)$  
          iff $B \mlim (A \mlim C)$
    \item $(A \mlcn \mltp) \mlim A$ and $A \mlim (A \mlcn \mltp)$
\bigskip
    \item[$(\parr,\mlze)$] is a symmetric monoidal structure
    \item $(A \mldn B) \mlim (B \mldn A)$
    \item $(A \mldn \mlze) \mlim A$ and $A \mlim (A \mldn \mlze)$
\bigskip
    \item[interaction] via either of 
\\[5px]
      \begin{tabular}[c]{ll}
      weak distributivity &
       $((A \mlcn B) \mldn C) \mlim (A \mlcn (B \mldn C))$
      \\[10px]
      Grishin(b) &
       $((A \mlim B) \mldn C) \mlim (A \mlim (B \mldn C))$
      \end{tabular}
\bigskip
    \item[Collapse to (classical)  MLL:] if we add converse of Grishin(b)
      \begin{tabular}[c]{l@{\extracolsep{1.6cm}}l}
      Grishin(a) &
       $(A \mlim (B \mldn C))  \mlim  ((A \mlim B) \mldn C)$
      \end{tabular}
 \end{description}

\end{frame}


\begin{frame}
  \frametitle{Proof Theory of Full Intuitionistic Linear Logic}
  
  \begin{description}[M]
  \item[$\ll$:] substructural logic without weakening and without contraction
  % \item[$\mill$:] $\mlcn \quad \mlim \quad 1
  %      \quad \Gamma \seq A$
  %      \hfill (intuitionistic)
  % \item[$\mll$:] $\ltens \quad \limp \quad 1 \quad \mldn \quad \bot$
  %      \hfill (classical)
  %  \item[$\fill$:] $\ltens \quad \limp \quad 1 \quad \mldn \quad \bot$
  %      \hfill (intuitionistic)
  \end{description}

\vfill
  \begin{tabular}{llll}
   %  Logic & Syntax & Sequents & Flavour
   % \\[8px]
    $\mill$ 
     &  $\mlcn \quad \mlim \quad 1$ 
%     &  single-conclusioned
     &  intuitionistic
     & cut-elimination
  \end{tabular}


     \[
       \AxiomC{$\Gamma_1 \sequent A$}
       \AxiomC{$\Gamma_2 \sequent B$}
      % \LeftLabel{($\mlcn$R)}
       \BinaryInfC{$\Gamma_1, \Gamma_2 \sequent  A \mlcn B$}
       \DisplayProof
        \qquad\qquad
             \AxiomC{$\Gamma, A \sequent B$}
      %\LeftLabel{$(\mlim R_1)$}
      \UnaryInfC{$\Gamma \sequent A \mlim B$}
      \DisplayProof
    \]

  \begin{tabular}{llll}
    \\
    $\mll$ 
     &  $\ltens \quad \limp \quad 1 \quad \mldn \quad \bot$
%     &  multiple conclusioned
     &  classical
     & cut-elimination
  \end{tabular}
\[
 \AxiomC{$\Gamma_1, A \sequent B, \Delta_1$}
 \AxiomC{$\Gamma_2, A \sequent B, \Delta_2$}
% \LeftLabel{($\mldn$R)}
 \BinaryInfC{$\Gamma_1 , \Gamma_2 \sequent \Delta_1 , A \mlcn B, \Delta_2$}
 \DisplayProof
\quad
 \AxiomC{$\Gamma \sequent A, B, \Delta$}
% \LeftLabel{$(\mlim R_2)$}
 \UnaryInfC{$\Gamma \sequent A \mldn B, \Delta$}
 \DisplayProof
\quad
 \AxiomC{$\Gamma, A \sequent B, \Delta$}
% \LeftLabel{$(\mlim R_2)$}
 \UnaryInfC{$\Gamma \sequent A \mlim B, \Delta$}
 \DisplayProof
\]

  \begin{tabular}{llll}
    \\
    $\fill$ 
     &  $\ltens \quad \limp \quad 1 \quad \mldn \quad \bot$
%     &  ?-conclusioned
     &  intuitionistic
     & cut-elimination fails
  \end{tabular}

\[
 \AxiomC{$\Gamma_1, A \sequent B, \Delta_1$}
 \AxiomC{$\Gamma_2, A \sequent B, \Delta_2$}
% \LeftLabel{($\mldn$R)}
 \BinaryInfC{$\Gamma_1 , \Gamma_2 \sequent \Delta_1 , A \mlcn B, \Delta_2$}
 \DisplayProof
\quad
 \AxiomC{$\Gamma \sequent A, B, \Delta$}
% \LeftLabel{$(\mlim R_2)$}
 \UnaryInfC{$\Gamma \sequent A \mldn B, \Delta$}
 \DisplayProof
%  \AxiomC{$\Gamma \sequent A_i$}
% % \LeftLabel{($\mldn$R)}
%  \UnaryInfC{$\Gamma \sequent A_1 \mldn A_2$}
%  \DisplayProof
\quad
% \imprightsc
 \AxiomC{$\Gamma, A \sequent B$}
% \LeftLabel{($\mldn$R)}
 \UnaryInfC{$\Gamma \sequent A \mlim B, \tblue{\Delta}$}
 \DisplayProof
\]

\end{frame}

\begin{frame}
  \frametitle{Problem and a solutions via annotated derivations}

  \begin{description}[M]
  \item[Remember:]  we need comma on the right to accommodate $\parr$
\vfill
  \item[Problem and existing solutions:] \    \\[5px]
    \hspace*{-0.5cm}
    \begin{tabular}{ccc}
      multiple conclusions & single conclusion & existing solutions
    \\[10px]
      \imprightmc & \imprightsc & 
         \AxiomC{$\Gamma , A \sequent B, \Delta$}
         % \LeftLabel{($\mldn$R)}
         \RightLabel{($\dagger$)}
        \UnaryInfC{$\Gamma \sequent A \mlim B, \Delta$}
       \DisplayProof
    \\[15px]
      unsound     & no cut-elimination & cut-elimination
    \\[5px]
    \end{tabular}
  \item[$\dagger$:] side-conditions which ensure that $A$ is
    ``independent'' of $\Delta$
\vfill
  \item[Hyland, de Paiva 1993:] type assignments to ensure that
    the variable typed by $A$ not appear free in the terms typed by $\Delta$

 %  \item[Bierman, Bellin:]
 %   $(a \parr b) \parr c \sequent a, ((b \parr c) \mlim d) \parr
 %   (e \mlim (d \parr e)$ had no cut-free derivation
 % refinements to fix bug which meant

 %  \item[Br\"auner and de Paiva:] annotate rules with a binary relation
 %    between antecedent formulae and succedent formulae,
 %    which effectively trace variable occurrence

  \end{description}
  
\end{frame}

\begin{frame}
  \frametitle{Further problems and solutions using annotations}

  \begin{description}[M]
%  \item[Remember:]  we need comma on the right to accommodate $\parr$
%\vfill
  \item[Hyland and de Paiva 1993:]
    \begin{tabular}{ccc}
%      multiple conclusions & single conclusion & existing solutions
%    \\[10px]
%      \imprightmc & \imprightsc & 
         \AxiomC{$\Gamma , A \sequent B, \Delta$}
         % \LeftLabel{($\mldn$R)}
         \RightLabel{($\dagger$)}
        \UnaryInfC{$\Gamma \sequent A \mlim B, \Delta$}
       \DisplayProof
    % \\[15px]
    %   unsound     & no cut-elimination & cut-elimination
 \\[10px]
    \end{tabular}
  % \item[$\dagger$:] side-conditions which ensure that $A$ is
  %   ``independent'' of $\Delta$
  \item[$\dagger$:] side-conditions which ensure that $A$ is
    ``independent'' of $\Delta$

  % \item[Hyland, de Paiva:] type assignments to ensure that
  %   the variable typed by $A$ not appear free in the terms typed by $\Delta$
\vfill
  \item[Bierman 1996:]
   $(a \parr b) \parr c \sequent a, ((b \parr c) \mlim d) \parr
   (e \mlim (d \parr e))$ has no cut-free derivation
   in the Hyland and de Paiva calculus

\vfill
  \item[Bierman, Bellin 1996:] refined annotations to regain cut-elimination

\vfill
  \item[Br\"auner and de Paiva 1997:] annotate rules with a binary relation
    between antecedent formulae and succedent formulae,
    which effectively trace variable occurrence
\vfill
\item What do derivations look like ?
  \end{description}
  
\end{frame}

\begin{frame}{Hyland , de Paiva and Biermann}
($\limp R$) legal as $v$ and $(w\parr x\limp y)
\parr z$ share no free variables.

\vfill

\hspace*{-1.2cm}
{\scriptsize
\AxiomC{$v:a\turn v:a$}
\AxiomC{$w:b\turn w:b$}
\BinaryInfC{$v\parr w:a\parr b\turn v:a,w:b$}
\AxiomC{$x:c\turn x:c$}
\BinaryInfC{$(v\parr w)\parr x:(a\parr b)\parr c \turn v:a,w:b,x:c$}
\UnaryInfC{$(v\parr w)\parr x:(a\parr b)\parr c \turn v:a,w\parr x:b\parr c$}
\AxiomC{$y:d\turn y:d$}
\BinaryInfC{$(v\parr w)\parr x:(a\parr b)\parr c,w\parr x\limp y:b\parr c\limp d\turn v: a,y:d$}
\AxiomC{$z:e\turn z:e$}
\BinaryInfC{$(v\parr w)\parr x:(a\parr b)\parr c,(w\parr x\limp y)\parr z:(b\parr c\limp d)\parr e\turn v:a,y:d,z:e$}
\UnaryInfC{$(v\parr w)\parr x:(a\parr b)\parr c,(w\parr x\limp y)\parr z:(b\parr c\limp d)\parr e\turn v:a,y\parr z:d\parr e$}
\UnaryInfC{$(v\parr w)\parr x:(a\parr b)\parr c\turn v:a,\lambda(w\parr x\limp y)\parr z^{(b\parr c\limp d)\parr e}.(y\parr z):(b\parr c\limp d)\parr e\tblue{\;\limp\;} d\parr e$}
\DisplayProof
}

\vfill
But the type annotations have no computational content

\end{frame}

\begin{frame}
  \frametitle{Bellin-style Proof}

 ($\limp R$) is legal because $r$ is not free in \texttt{$\mbox{let }
t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be }v\parr\mbox{- in }v$} 
% We apologise
% for the extremely small font size necessary to fit this proof on the page.

\vfill
\hspace*{-4cm}
{\tiny
\AxiomC{$v:a\turn v:a$}
\AxiomC{$w:b\turn w:b$}
\BinaryInfC{$u:a\parr b\turn \mbox{let }u\mbox{ be }v\parr\mbox{- in }v:a,\mbox{let }u\mbox{ be -}\parr w\mbox{ in }w:b$}
\AxiomC{$x:c\turn x:c$}
\BinaryInfC{$t:(a\parr b)\parr c \turn \mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be }v\parr\mbox{- in }v:a,\mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be -}\parr w\mbox{ in }w:b,\mbox{let }t\mbox{ be -}\parr x\mbox{ in }x:c$}
\UnaryInfC{$t:(a\parr b)\parr c \turn \mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be }v\parr\mbox{- in }v:a,(\mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be -}\parr w\mbox{ in }w)\parr(\mbox{let }t\mbox{ be -}\parr x\mbox{ in }x):b\parr c$}
\AxiomC{$y:d\turn y:d$}
\BinaryInfC{$t:(a\parr b)\parr c,s:b\parr c\limp d\turn  \mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be }v\parr\mbox{- in }v:a,(s(\mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be -}\parr w\mbox{ in }w)\parr(\mbox{let }t\mbox{ be -}\parr x\mbox{ in }x)):d$}
\AxiomC{$z:e\turn z:e$}
\BinaryInfC{$t:(a\parr b)\parr c,r:(b\parr c\limp d)\parr e\turn  \mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be }v\parr\mbox{- in }v:a,\mbox{let } r\mbox{ be }s\parr\mbox{- in }(s(\mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be -}\parr w\mbox{ in }w)\parr(\mbox{let }t\mbox{ be -}\parr x\mbox{ in }x)):d,\mbox{let }s\mbox{ be -}\parr z\mbox{ in }z:e$}
\UnaryInfC{$t:(a\parr b)\parr c,r:(b\parr c\limp d)\parr e\turn  \mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be }v\parr\mbox{- in }v:a,(\mbox{let } r\mbox{ be }s\parr\mbox{- in }(s(\mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be -}\parr w\mbox{ in }w)\parr(\mbox{let }t\mbox{ be -}\parr x\mbox{ in }x)))\parr(\mbox{let }s\mbox{ be -}\parr z\mbox{ in }z):d\parr e$}
\UnaryInfC{$t:(a\parr b)\parr c\turn \mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be }v\parr\mbox{- in }v:a,\lambda r^{(b\parr c\limp d)\parr e}.(\mbox{let } r\mbox{ be }s\parr\mbox{- in }(s(\mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be -}\parr w\mbox{ in }w)\parr(\mbox{let }t\mbox{ be -}\parr x\mbox{ in }x)))\parr(\mbox{let }s\mbox{ be -}\parr z\mbox{ in }z):(b\parr c\limp d)\parr e\limp d\parr e$}
\DisplayProof
}

\vfill
Again, the type annotations are not given any computational content
and this derivation does not even fit on the page!  
\end{frame}

\begin{frame}
  \frametitle{Br\"{a}uner and de Paiva-style proof}
  
($\limp R$) legal because $(b\parr c
\limp d)\parr e$ is not related to $a$

\vfill
\hspace*{-6cm}
{\scriptsize
\AxiomC{ \ }\LeftLabel{$(a,a)$\;}
\UnaryInfC{$a\turn a$}
\AxiomC{ \ }\RightLabel{\;$(b,b)$}
\UnaryInfC{$b\turn b$}\LeftLabel{$(a\parr b,a),(a\parr b,b)$\;}
\BinaryInfC{$a\parr b\turn a,b$}
\AxiomC{ \ }\RightLabel{\;$(c,c)$}
\UnaryInfC{$c\turn c$}\LeftLabel{$((a\parr b)\parr c,a),((a\parr b)\parr c,b),((a\parr b)\parr c,c)$\;}
\BinaryInfC{$(a\parr b)\parr c \turn a,b,c$}\LeftLabel{$((a\parr b)\parr c,a),((a\parr b)\parr c,b\parr c)$\;}
\UnaryInfC{$(a\parr b)\parr c \turn a,b\parr c$}
\AxiomC{ \ }\LeftLabel{$(d,d)$}
\UnaryInfC{$d\turn d$}\LeftLabel{$((a\parr b)\parr c,a),((a\parr b)\parr c,d),(b\parr c\limp d,d)$\;}
\BinaryInfC{$(a\parr b)\parr c,b\parr c\limp d\turn a,d$}
\AxiomC{ \ }\LeftLabel{\;$(e,e)$}
\UnaryInfC{$e\turn e$}\LeftLabel{$((a\parr b)\parr c,a),((a\parr b)\parr c,d),((b\parr c\limp d)\parr e,d),((b\parr c\limp d)\parr e,e)$\;}
\BinaryInfC{$(a\parr b)\parr c,(b\parr c\limp d)\parr e\turn a,d,e$}\LeftLabel{$((a\parr b)\parr c,a),((a\parr b)\parr c,d\parr e),((b\parr c\limp d)\parr e,d\parr e)$\;}
\UnaryInfC{$(a\parr b)\parr c,(b\parr c\limp d)\parr e\turn a,d\parr e$}\LeftLabel{$((a\parr b)\parr c,a),((a\parr b)\parr c,(b\parr c\limp d)\parr e\limp d\parr e)$\;}
\UnaryInfC{$(a\parr b)\parr c\turn a,(b\parr c\limp d)\parr e\tblue{\;\limp\;} d\parr e$}
\DisplayProof
}

\vfill
Pure annotational device to track variable occurrences
\end{frame}

\begin{frame}{Cut-free derivation in our display calculus}

  \begin{center}
{\small
\AxiomC{$a\turn a$}
\AxiomC{$b\turn b$}%\LeftLabel{\scriptsize{($\parr\turn$)}}
\BinaryInfC{$a\parr b\turn a,b$}
\AxiomC{$c\turn c$}%\LeftLabel{\scriptsize{($\parr\turn$)}}
\BinaryInfC{$(a\parr b)\parr c \turn a,b,c$} %\LeftLabel{\scriptsize{\textbf{(drp)}}}
\UnaryInfC{$(a\parr b)\parr c<a \turn b,c$} %\LeftLabel{\scriptsize{($\turn\parr$)}}
\UnaryInfC{$(a\parr b)\parr c<a\turn b\parr c$}
\AxiomC{$d\turn d$}%\LeftLabel{\scriptsize{($\limp\turn$)}}
\BinaryInfC{$b\parr c\limp d \turn ((a\parr b)\parr c<a)>d$}
\AxiomC{$e\turn e$}%\LeftLabel{\scriptsize{($\parr\turn$)}}
\BinaryInfC{$(b\parr c\limp d)\parr e \turn (((a\parr b)\parr c<a)>d),e$}%\LeftLabel{\scriptsize{($\turn$ Grnb)}}
\UnaryInfC{$(b\parr c\limp d)\parr e \turn ((a\parr b)\parr c<a)>d,e$}%\LeftLabel{\scriptsize{(rp)}}
\UnaryInfC{$(b\parr c\limp d)\parr e,((a\parr b)\parr c<a)\turn d,e$}%\LeftLabel{\scriptsize{($\turn\parr$)}}
\UnaryInfC{$(b\parr c\limp d)\parr e, ((a\parr b)\parr c<a) \turn d\parr e$}%\LeftLabel{\scriptsize{(rp)}}
\UnaryInfC{$(a\parr b)\parr c<a \turn (b\parr c\limp d)\parr
    e > d\parr e$}%%\LeftLabel{\scriptsize{($\turn\limp$)}}
\UnaryInfC{$(a\parr b)\parr c < a \turn (b\parr c\limp d)\parr e \limp d\parr e$}%\LeftLabel{\scriptsize{\textbf{(drp)}}}
\UnaryInfC{$(a\parr b)\parr c \turn a, (b\parr c\limp d)\parr e\limp d\parr e$}
\DisplayProof
}
    \end{center}


No annotations, but many extra structural connectives

\end{frame}

\begin{frame}{Cut-free derivation in the deep nested calculus}


%  \begin{center}
%{\scriptsize
$$
\hspace*{-0.60cm}
\infer%[\limp_r^d]
{(a \parr b) \parr c \seq a, {(b \parr c \limp d) \parr e \limp d \parr e} }
{
 \infer%[\parr_r^d]
 { (a \parr b) \parr c \seq a, ((b \parr c \limp d) \parr e \seq {d \parr e})}
 {
  \infer%[\parr_l^d]
  { (a \parr b) \parr c \seq a, ({(b \parr c \limp d) \parr e} \seq d, e)}
  {
   \infer%[\limp_l^d]
   {(a \parr b) \parr c \seq a, ({b \parr c \limp d} \seq d)} 
   {
    \infer%[\parr_r^d]
    {(a \parr b) \parr c \seq a, (\sunit \seq {b \parr c})} 
    {
     \infer%[\parr_l^d]
     {{(a \parr b) \parr c} \seq a, (\sunit \seq b, c)} 
     {
      \infer%[\parr_l^d]
      {{a \parr b} \seq a, (\sunit \seq b)}
      {
        \infer%[id^d]
        {a \seq a, (\sunit \seq \sunit)}
        { }
        &
        \infer%[pl_1]
        {b \seq (\sunit \seq b)}
        {
           \infer%[id^d]
           {\sunit \seq (b \seq b)}{}
        }
      }
      &
      \infer%[pl_1]
      {c \seq (\sunit \seq c)}
      {
       \infer%[id^d]
       {\sunit \seq (c \seq c)}
       {}
      }
     }
    }
    &
    \!\!
    \infer%[id^d]
    {\sunit \seq (d \seq d)}
    {}
   }
   &
   \infer%[id^d]
   { \sunit \seq (e \seq e)}
   {}
  }
 } 
}
$$
%}
%  \end{center}

No annotations, only commas as structural connective, but sequents are nested
$(\cdots \seq \cdots) \cdots \seq \cdots (\cdots \seq \cdots)$
\end{frame}

\begin{frame}
  \frametitle{Display calculus for (an extension of) $\fill$}

  \begin{description}[M]
  % \item[$\biill$:] extension of ILL with a connective adjoint to $\mldn$
  %   \begin{eqnarray*}
  %     \label{eq:1}
  %     (A \mlcn B) \mlim C & iff & A \mlim (B \mlim C) 
  %    \\
  %     (A \excl B) \mlim C & iff & A \mlim (B \mldn C) 
  %   \end{eqnarray*}
%  \item[Formula:] $A$ %\hfill   \tblue{Structural Constant:} $\Phi$
  \item[Structural Constant and Binary Connectives:] $\Phi \qquad , \qquad < \qquad >$
  \item[Antecedent Structure:]
     $X_a~~Y_a ::= A \mid \Phi \mid X_a,Y_a \mid X_a<Y_s$
  \item[Succcedent Structure:]
     $  X_s~~Y_s ::= A \mid \Phi \mid X_s,Y_s \mid X_a>Y_s$
   \item[Sequent:] $X_a \vdash Y_s$ 
       \hfill (drop subscripts to avoid clutter)
\vfill
   \item[Display Postulates:] reversible structural rules
   \[
          \AxiomC{$X_a \sequent Y_a > Z_s$}
           \doubleLine
           \UnaryInfC{$X_a , Y_a \sequent Z_s$}
           \doubleLine
           \UnaryInfC{$Y_a \sequent X_a > Z_s$}
 \DisplayProof
\qquad\qquad\qquad\qquad
   \AxiomC{$Z_a < Y_s \sequent X_s$}
   \doubleLine
 \UnaryInfC{$Z_a \sequent X_s , Y_s$}
 \doubleLine
 \UnaryInfC{$Z_a < X_s \sequent Y_s$}
 \DisplayProof
   \]
\vfill
 \item[Display Property:] For every antecedent (succedent) part $Z$ of
   the sequent $X \turn Y$, there is a sequent $Z \turn Y'$ (resp. $X'
   \turn Z$) obtainable from $X \turn Y$ using only the display
   postulates, thereby displaying the $Z$ as the whole of one side
  \end{description}

\end{frame}

\begin{frame}
  \frametitle{Logical rules: introduced formula is always displayed}
  
{\small
  \begin{tabular}[l]{l@{\extracolsep{1.5cm}}l}
  \AxiomC{(id)\quad$p\turn p$}
  \DisplayProof
  &
  \AxiomC{$X\turn A$}
  \AxiomC{$A\turn Y$}
  \LeftLabel{(cut)\,}
  \BinaryInfC{$X\turn Y$}
  \DisplayProof
\\[10px]
  \AxiomC{$\Phi\turn X$}
  \LeftLabel{($\mltp\turn$)\,}
  \UnaryInfC{$\mltp\turn X$}
  \DisplayProof
  &
  \AxiomC{($\turn \mltp$)\quad$\Phi\turn \mltp$}
  \DisplayProof
\\[10px]
  \AxiomC{($\mlze\turn$)\quad$\mlze\turn\Phi$}
  \DisplayProof
  &
  \AxiomC{$X\turn\Phi$}
  \LeftLabel{($\turn\mlze$)\,}
  \UnaryInfC{$X\turn\mlze$}
  \DisplayProof
\\[12px]
  \AxiomC{$A,B\turn X$}
  \LeftLabel{($\otimes\turn$)\,}
  \UnaryInfC{$A\otimes B\turn X$}
  \DisplayProof
  &
  \AxiomC{$X\turn A$}
  \AxiomC{$Y\turn B$}
  \LeftLabel{($\turn\otimes$)\,}
  \BinaryInfC{$X,Y\turn A\otimes B$}
  \DisplayProof
\\[12px]
  \AxiomC{$A\turn X$}
  \AxiomC{$B\turn Y$}
  \LeftLabel{($\parr\turn$)\,}
  \BinaryInfC{$A\parr B\turn X,Y$}
  \DisplayProof
  &
  \AxiomC{$X\turn A,B$}
  \LeftLabel{($\turn\parr$)\,}
  \UnaryInfC{$X\turn A\parr B$}
  \DisplayProof
\\[12px]
  \AxiomC{$X\turn A$}
  \AxiomC{$B\turn Y$}
  \LeftLabel{($\limp\turn$)\,}
  \BinaryInfC{$A\limp B\turn X>Y$}
  \DisplayProof
  &
  \AxiomC{$X\turn A>B$}
  \LeftLabel{($\turn\limp$)\,}
  \UnaryInfC{$X\turn A\limp B$}
  \DisplayProof
\\[12px]
  \AxiomC{$A<B\turn X$}
    \LeftLabel{\tblue{($\excl\turn$)}\,}
  \UnaryInfC{$A\excl B\turn X$}
  \DisplayProof
  &
  \AxiomC{$X\turn A$}
  \AxiomC{$B\turn Y$}
  \LeftLabel{\tblue{($\turn\excl$)}\,}
  \BinaryInfC{$X<Y\turn A\excl B$}
  \DisplayProof
  \end{tabular}
}
\vfill
read upwards, one rule is a ``rewrite'' while other ``constrains''
\end{frame}

\begin{frame}
  \frametitle{Structural rules: no occurrences of formula meta-variables}
  
all sub-structural properties captured in a modular way

\vfill
{\small
  \begin{tabular}[c]{l@{\extracolsep{0.5cm}}l}
% \multicolumn{2}{c}{
%   \AxiomC{$X\turn Y>Z$}
%   \doubleLine
%   \LeftLabel{(rp)\,}
%   \UnaryInfC{$X,Y\turn Z$}
%   \DisplayProof
%   \qquad
%   \AxiomC{$X, Y \turn Z$}
%   \doubleLine
%   \LeftLabel{(rp)\,}
%   \UnaryInfC{$Y\turn X>Z$}
%   \DisplayProof
%   \qquad
%   \AxiomC{$X<Y\turn Z$}
%   \doubleLine
%   \LeftLabel{(drp)\,}
%   \UnaryInfC{$X\turn Y,Z$}
%   \DisplayProof
%   \qquad
%   \AxiomC{$X \turn Y,Z$}
%   \doubleLine
%   \LeftLabel{(drp)\,}
%   \UnaryInfC{$X<Z\turn Y$}
%   \DisplayProof
% }
%\\[15px]
  \AxiomC{$X,\Phi\turn Y$}
  \doubleLine
  \LeftLabel{($\Phi\turn$)\,}
  \UnaryInfC{$X\turn Y$}
  \DisplayProof
  &
  \AxiomC{$X\turn \Phi,Y$}
  \doubleLine
  \LeftLabel{($\turn\Phi$)\,}
  \UnaryInfC{$X\turn Y$}
  \DisplayProof
\\[15px]
  \AxiomC{$W,(X,Y)\turn Z$}
  \doubleLine
  \LeftLabel{(Ass $\turn$)\,}
  \UnaryInfC{$(W,X),Y\turn Z$}
  \DisplayProof
  &
  \AxiomC{$W\turn (X,Y),Z$}
  \doubleLine
  \LeftLabel{($\turn$ Ass)\,}
  \UnaryInfC{$W\turn X,(Y,Z)$}
  \DisplayProof
\\[15px]
  \AxiomC{$X,Y\turn Z$}
  \LeftLabel{(Com $\turn$)\,}
  \UnaryInfC{$Y,X\turn Z$}
  \DisplayProof
  &
  \AxiomC{$Z\turn Y,X$}
  \LeftLabel{($\turn$ Com)\,}
  \UnaryInfC{$Z\turn X,Y$}
  \DisplayProof
\\[15px]
% \multicolumn{2}{c}{
%   \AxiomC{$W\vdash (X> Y), Z$}
%     \LeftLabel{(Grnb)}
%   \UnaryInfC{$W\vdash X>(Y,Z)$}
% \DisplayProof
% }
  \AxiomC{$W,(X<Y)\turn Z$}
    \LeftLabel{(Grnb $\turn$)}
  \UnaryInfC{$(W,X)<Y\turn Z$}
  \DisplayProof
  &
  \AxiomC{$W\vdash (X> Y), Z$}
    \LeftLabel{($\turn$ Grnb)}
  \UnaryInfC{$W\vdash X>(Y,Z)$}
  \DisplayProof
\\[30px]
% {\small
%    $ (A \mlcn B) \mldn C) \mlim (A \mlcn (B \mldn C))$
% }   
  &
{\small
   $((A \mlim B) \mldn C) \mlim (A \mlim (B \mldn C))$
}  
\end{tabular}
}
\end{frame}

\begin{frame}{Example derivation in our display calculus}

{\small
\AxiomC{$a\turn a$}
\AxiomC{$b\turn b$}\LeftLabel{\scriptsize{($\parr\turn$)}}
\BinaryInfC{$a\tgreen{\;\parr\;} b\turn a,b$}
\AxiomC{$c\turn c$}\LeftLabel{\scriptsize{($\parr\turn$)}}
\BinaryInfC{$(a\parr b)\tred{\;\parr\;} c \turn \tblue{(a,b)},c$} \LeftLabel{\scriptsize{\textbf{(ass)}}}
\UnaryInfC{$(a\parr b)\parr c \turn a,(b,c)$} \LeftLabel{\scriptsize{\textbf{(drp)}}}
\UnaryInfC{$(a\parr b)\parr c\tred{\;<\;}a \turn \tblue{b,c}$} \LeftLabel{\scriptsize{($\turn\parr$)}}
\UnaryInfC{$(a\parr b)\parr c<a\turn \tblue{b\parr c}$}
\AxiomC{$d\turn d$}\LeftLabel{\scriptsize{($\limp\turn$)}}
\BinaryInfC{$b \parr c \tred{\;\limp\;} d \turn ((a\parr b)\parr c<a)\tred{\;>\;}d$}
\AxiomC{$e\turn e$}\LeftLabel{\scriptsize{($\parr\turn$)}}
\BinaryInfC{$(b\parr c\limp d)\tgreen{\;\parr\;} e \turn \tblue{(}((a\parr b)\parr c<a)>d\tblue{)},e$}\LeftLabel{\scriptsize{\tblue{($\turn$ Grnb)}}}
\UnaryInfC{$(b\parr c\limp d)\parr e \turn ((a\parr b)\parr c<a)\tred{\;>\;}(d,e)$}\LeftLabel{\scriptsize{(rp)}}
\UnaryInfC{$(b\parr c\limp d)\parr e\tred{,}((a\parr b)\parr c<a)\turn \tblue{d,e}$}\LeftLabel{\scriptsize{($\turn\parr$)}}
\UnaryInfC{$\tgreen{(b\parr c\limp d)\parr e},((a\parr b)\parr c<a)\turn \tblue{d\parr e}$}\LeftLabel{\scriptsize{(rp)}}
\UnaryInfC{$(a\parr b)\parr c<a \turn \tgreen{(b\parr c\limp d)\parr e}\tred{\;>\;}(d\parr e)$}\LeftLabel{\scriptsize{\tblue{($\turn\limp$)}}}
\UnaryInfC{$(a\parr b)\parr c\tblue{\;<a} \turn (b\parr c\limp d)\parr e\tred{\;\limp\;} (d\parr e)$}\LeftLabel{\scriptsize{\textbf{(drp)}}}
\UnaryInfC{$(a\parr b)\parr c \turn \tblue{a,}(b\parr c\limp d)\parr e\limp (d\parr e)$}
\DisplayProof
}

\vfill
But we implicitly created an occurrence of $\excl$ via $\tblue{<}$
\end{frame}

\begin{frame}
  \frametitle{Categorial semantics for bi-intuitionistic linear logic $\biill$}

 \begin{description}[M]
    \item[$(\mlcn,\mltp,\mlim)$] is a symmetric monoidal closed structure 
    \item $A \mlcn B \mlim C$ 
          iff $A \mlim (B \mlim C)$  
          iff $B \mlim (A \mlim C)$
    \item $(A \mlcn \mltp) \mlim A$ and $A \mlim (A \mlcn \mltp)$
\bigskip
    \item[$(\mllx,\parr,\mlze)$] is a symmetric monoidal co-closed structure
%    \item $(A \mldn B) \mlim (B \mldn A)$
    \item $A \mlim (B \mldn C)$ 
          iff $(A \mllx B) \mlim C$  
          iff $(A \mllx C) \mlim B$
    \item $(A \mldn \mlze) \mlim A$ and $A \mlim (A \mldn \mlze)$
\bigskip
    \item[interaction] via either of 
\\[5px]
      \begin{tabular}[c]{ll}
      % weak distributivity &
      %  $(A \mlcn B) \mldn C) \mlim (A \mlcn (B \mldn C))$
      % \\[10px]
      Grishin(b) &
       $((A \mlim B) \mldn C) \mlim (A \mlim (B \mldn C))$
      \\[10px]
      dualGrishin(b) &
       $((A \mlcn B) \mllx C) \mlim (A \mlcn (B \mllx C))$
      \\[10px]
      \end{tabular}
\bigskip
    \item[Collapse to (classical)  MLL:] if we add converse of either
%     Grishin(b)
      % \begin{tabular}[c]{l@{\extracolsep{1.6cm}}l}
      % Grishin(a) &
      %  $(A \mlim (B \mldn C))  \mlim  ((A \mlim B) \mldn C)$
      % \end{tabular}
 \end{description}

\end{frame}

% \begin{frame}
%   \frametitle{Categorial Semantics for $\biill$}

%   \begin{description}[M]
%   \item[A \emph{FILL-category}] is a category equipped with
%     \begin{itemize}
%     \item a symmetric monoidal closed structure $(\otimes,I,\limp)$
%     \item a symmetric monoidal structure $(\parr,\bot)$
%     \item a natural family of \emph{weak distributivity} arrows
%       $A\otimes(B\parr C)\to(A\otimes B)\parr C$.
%     \end{itemize}

% \vfill
% \item[A \emph{BiILL-category}] is a FILL-category where the $\parr$
%   bifunctor has a \emph{co-closure} $\excl$, so there is a natural
%   isomorphism between arrows $A \to B\parr C$ and $A\excl B\to C$.

% \vfill
% \item[Validity:] A FILL/BiILL sequent $X\turn Y$ is
%   \emph{valid} if for every FILL- (resp.\ BiILL-) category and any
%   valuation of its propositional variables as objects, there exists an
%   arrow 
%
%
  %$I\to\tau^a(X)\limp\tau^s(Y)$.
  %(equivalently, an arrow 
%  $\tau^a(X)\to\tau^s(Y)$. %).
  % It is FILL- (resp. BiILL-) \emph{valid} if
  % it is satisfied by all such categories. In fact, we only need to
  % check the free categories under their generic valuations.

% %These categorical notions can all be formulated as the requirement
% %that a certain inductively defined set of arrows exists (satisfying certain
% %equations). In particular, the \emph{free} FILL- (resp. BiILL-) category has as
% %objects FILL- (resp. BiILL-) formulae, and as arrows only those required by the
% %definition (quotiented by the required equations).
%  \end{description}

% \begin{definition}\label{def:free}
%   The \emph{free} FILL- (resp. BiILL-) category has FILL- (resp.
%   BiILL-) formulae as objects and the following arrows (quotiented by
%   certain equations) where we are given objects $A, A',A'',B,B'$ and
%   arrows $f:A\to A',f':A'\to A'',g:B\to B'$,
%   $(\binop,K)\in\{(\otimes,I),(\parr,\bot)\}$, and where the
%   co-closure arrows exist in the free BiILL-category only:
% \begin{description}[M]
% \item[Category:] 
%   $\xymatrix{A \ar[r]^{id} & A}
%   \qquad
%   \xymatrix{A \ar[r]^-{f'\circ f} & A''}$
% \item[Symmetric Monoidal:]
%   $\xymatrix{A\binop B \ar[r]^-{f\binop g} & A'\binop B'}
%    \qquad
%   \xymatrix{(A\binop B)\binop C \ar@<0.5ex>[r]^{\alpha} & A\binop(B\binop C)
%   \ar@<0.5ex>[l]^{\alpha^{-1}}}
%   $   
% \item[\hphantom{Symmetric Monoidal:}]
%   $
%   \xymatrix{K\binop A \ar@<0.5ex>[r]^-{\lambda} & A
%   \ar@<0.5ex>[l]^-{\lambda^{-1}}}
%   \qquad
%   \xymatrix{A\binop K \ar@<0.5ex>[r]^-{\rho} & A \ar@<0.5ex>[l]^-{\rho^{-1}}}
%   \qquad
%   \xymatrix{A\binop B \ar[r]^{\gamma} & B\binop A}
%   $
% \item[Closed:] 
%   $\xymatrix{A\limp B \ar[r]^-{A\limp g} & A\limp B'}
%    \qquad
%    \xymatrix{(A\limp B)\otimes A \ar[r]^-{\varepsilon} & B}
%    \qquad
%   \xymatrix{A \ar[r]^-{\eta} & B\limp A\otimes B}$
% \item[Weak Distributivity:]
%   $\xymatrix{A\otimes(A'\parr A'') \ar[r]^{\omega} & (A\otimes A')\parr A''}$
% \item[Co-Closed:] 
%   $\xymatrix{A\excl B \ar[r]^-{f\excl B} & A'\excl B}
%    \qquad
%    \xymatrix{A\parr B\excl A \ar[r]^-{\varepsilon} & B}
%    \qquad
%    \xymatrix{A \ar[r]^-{\eta} & B\parr(A\excl B)}$
% \end{description}
% \end{definition}

%\end{frame}

\begin{frame}
  \frametitle{Soundness, completeness and cut-elimination}
  
  \begin{description}[M]
  \item[Thm:] The sequent $X \vdash Y$ is derivable iff  the
    formula-translation $\tau_a(X) \mlim \tau_s(Y)$ is $\biill$-valid
 \item[Proof:] the display calculus proof rules and the arrows of the
   free BiILL-category are inter-definable.
%  \end{description}
% \end{frame}

% \begin{frame}
%   \frametitle{Cut-elimination}
  
%   \begin{description}[M]
\vfill
    \item[Thm:] If $X \sequent Y$ is
      derivable then it is cut-free derivable.
    \item[Proof:] The rules obey conditions C1-C8 given by Belnap (1982),
      hence the calculus enjoys cut-admissibility
\vfill
    \item[Method:] Essentially Gentzen's original method
      \begin{description}[M]
      \item[Left-principal cuts:] turned into left and right
        principal cuts
      \item[Right-principal cuts:] turned into left and right
        principal cuts
      \item[Left\&right principal cuts:] replaced by multiple
        ``smaller'' cuts
      \item[Need:] substitution principles guaranteed by
        display property and explicit structural rules
      \item[Termination:] double induction on grade and size of cut-formula
      \end{description}
  \end{description}
\end{frame}

\begin{frame}
  \frametitle{Proof search via display calculi}
  
Given end-sequent $X \vdash Y$ how to find a derivation?

\vfill
Apply (invertible) ``rewrite'' rules immediately

\vfill
For  ``constraint'' rules, use structural rules to match structure

% \vfill
% But  there are just too many possibilities for this to be efficient

% \vfill
% Need to compile ``display'',  ``undisplay'' and ``structural rules''
% into the logical rules as much as possible (maintaining cut-elimination)
\end{frame}

\begin{frame}{Backward Proof-search for display calculus}

{\small
\AxiomC{$a\turn a$}
\AxiomC{$b\turn b$}%\LeftLabel{\scriptsize{($\parr\turn$)}}
\BinaryInfC{$a\tgreen{\;\parr\;} b\turn a,b$}
\AxiomC{$c\turn c$}%\LeftLabel{\scriptsize{($\parr\turn$)}}
\BinaryInfC{$(a\parr b)\tred{\;\parr\;} c \turn \tblue{(a,b)},c$}% \LeftLabel{\scriptsize{\textbf{(?)}}}
\UnaryInfC{$(a\parr b)\parr c \turn a,(b,c)$} \LeftLabel{\scriptsize{\textbf{(?)}}}
\UnaryInfC{$(a\parr b)\parr c\tred{\;<\;}a \turn \tblue{b,c}$} \LeftLabel{\scriptsize{($\turn\parr$)}}
\UnaryInfC{$(a\parr b)\parr c<a\turn \tblue{b\parr c}$}
\AxiomC{$d\turn d$}\LeftLabel{\scriptsize{($\limp\turn$)}}
\BinaryInfC{$b \parr c \tred{\;\limp\;} d \turn ((a\parr b)\parr c<a)\tred{\;>\;}d$}
\AxiomC{$e\turn e$}\LeftLabel{\scriptsize{($\parr\turn$)}}
\BinaryInfC{$(b\parr c\limp d)\tgreen{\;\parr\;} e \turn \tblue{(}((a\parr b)\parr c<a)>d\tblue{)},e$}\LeftLabel{\scriptsize{\tblue{(?)}}}
\UnaryInfC{$(b\parr c\limp d)\parr e \turn ((a\parr b)\parr c<a)\tred{\;>\;}(d,e)$}\LeftLabel{\scriptsize{(?)}}
\UnaryInfC{$(b\parr c\limp d)\parr e\tred{,}((a\parr b)\parr c<a)\turn \tblue{d,e}$}\LeftLabel{\scriptsize{($\turn\parr$)}}
\UnaryInfC{$\tgreen{(b\parr c\limp d)\parr e},((a\parr b)\parr c<a)\turn \tblue{d\parr e}$}\LeftLabel{\scriptsize{(?)}}
\UnaryInfC{$(a\parr b)\parr c<a \turn \tgreen{(b\parr c\limp d)\parr e}\tred{\;>\;}(d\parr e)$}\LeftLabel{\scriptsize{\tblue{($\turn\limp$)}}}
\UnaryInfC{$(a\parr b)\parr c\tblue{\;<a} \turn (b\parr c\limp d)\parr e\tred{\;\limp\;} (d\parr e)$}\LeftLabel{\scriptsize{\textbf{(?)}}}
\UnaryInfC{$(a\parr b)\parr c \turn \tblue{a,}(b\parr c\limp d)\parr e\limp (d\parr e)$}
\DisplayProof
}

\end{frame}

\begin{frame}
  \frametitle{Proof search via display calculi}
  
Given end-sequent $X \vdash Y$ how to find a derivation?

\vfill
Apply (invertible) ``rewrite'' rules immediately

\vfill
For  ``constraint'' rules, use structural rules to match structure

\vfill
But  there are just too many possibilities for this to be efficient

\vfill
Need to compile ``display'',  ``undisplay'' and ``structural rules''
into the logical rules as much as possible (maintaining cut-elimination)
\end{frame}

\begin{frame}{Cut-free derivation in the deep nested calculus}


%  \begin{center}
%{\scriptsize
$$
\hspace*{-0.60cm}
\infer%[\limp_r^d]
{(a \parr b) \parr c \seq a, {(b \parr c \limp d) \parr e \limp d \parr e} }
{
 \infer%[\parr_r^d]
 { (a \parr b) \parr c \seq a, ((b \parr c \limp d) \parr e \seq {d \parr e})}
 {
  \infer%[\parr_l^d]
  { (a \parr b) \parr c \seq a, ({(b \parr c \limp d) \parr e} \seq d, e)}
  {
   \infer%[\limp_l^d]
   {(a \parr b) \parr c \seq a, ({b \parr c \limp d} \seq d)} 
   {
    \infer%[\parr_r^d]
    {(a \parr b) \parr c \seq a, (\sunit \seq {b \parr c})} 
    {
     \infer%[\parr_l^d]
     {{(a \parr b) \parr c} \seq a, (\sunit \seq b, c)} 
     {
      \infer%[\parr_l^d]
      {{a \parr b} \seq a, (\sunit \seq b)}
      {
        \infer%[id^d]
        {a \seq a, (\sunit \seq \sunit)}
        { }
        &
        \infer%[pl_1]
        {b \seq (\sunit \seq b)}
        {
           \infer%[id^d]
           {\sunit \seq (b \seq b)}{}
        }
      }
      &
      \infer%[pl_1]
      {c \seq (\sunit \seq c)}
      {
       \infer%[id^d]
       {\sunit \seq (c \seq c)}
       {}
      }
     }
    }
    &
    \!\!
    \infer%[id^d]
    {\sunit \seq (d \seq d)}
    {}
   }
   &
   \infer%[id^d]
   { \sunit \seq (e \seq e)}
   {}
  }
 } 
}
$$
%}
%  \end{center}

No annotations, only commas as structural connective, but sequents are
nested 
\end{frame}

\begin{frame}
  \frametitle{Nested sequent calculi: Kashima 1994 (for tense logics)}

  \begin{description}[M]
 \item[Nested sequent:] where comma is associative and commutative
  $$
  S~~T \;::=\; S_1,\dots,S_k,A_1,\dots,A_m \seq B_1,\dots, B_n, T_1, \dots,T_l
  $$

\item[Context:] nested sequent with exactly one hole $[~]$
\item[Positive/Negative:] if $[~]$ occurs immediately to 
  right/left of $\seq$


%\vfill
% \item[Shallow nested sequent calculus:] Notational variant of display
%   calculi where all occurrences of $\turn$ and $<$ and $>$ are
%   replaced by $\seq$ and associativity and commutativity of comma are
%   built-in

\vfill
\item[Turn Rules:] reversible rules using \textbf{multisets} of 
     nested sequents and formulae
   \[
% \hspace*{-1cm}
%           \AxiomC{$X_a \sequent Y_a > Z_s$}
%            \doubleLine
%            \UnaryInfC{$X_a , Y_a \sequent Z_s$}
%            \doubleLine
%            \UnaryInfC{$Y_a \sequent X_a > Z_s$}
%            \DisplayProof
% \quad
          \AxiomC{$\Sc_2 \seq (\Sc_1 \seq \Tc)$}
           \doubleLine
           \UnaryInfC{$\Sc_1 , \Sc_2 \seq \Tc$}
           % \doubleLine
           % \UnaryInfC{$S_1 \seq (S_2 \seq T)$}
           \DisplayProof
\qquad\qquad\qquad\qquad
           \AxiomC{$(\Sc \seq \Tc_2) \seq \Tc_1$}
           \doubleLine
           \UnaryInfC{$\Sc \seq (\Tc_1 , \Tc_2)$}
           % \doubleLine
           % \UnaryInfC{$(S \seq T_1) \seq T_2$}
           \DisplayProof
% \quad
%            \AxiomC{$Z_a < Y_s \sequent X_s$}
%            \doubleLine
%            \UnaryInfC{$Z_a \sequent X_s , Y_s$}
%            \doubleLine
%            \UnaryInfC{$Z_a < X_s \sequent Y_s$}
%            \DisplayProof
   \]

% To go back, compute whether a given $\seq$ is an
% ``antecedent'' or ``succedent'' part, and replace it with $<$ or $>$
% as appropriate.

\pause
   \[
\hspace*{-1cm}
          \AxiomC{$X_a \sequent Y_a > Z_s$}
           \doubleLine
           \UnaryInfC{$X_a , Y_a \sequent Z_s$}
           \doubleLine
           \UnaryInfC{$Y_a \sequent X_a > Z_s$}
           \DisplayProof
% \quad
          % \AxiomC{$\Sc_2 \seq (\Sc_1 \seq \Tc)$}
          %  \doubleLine
          %  \UnaryInfC{$\Sc_1 , \Sc_2 \seq \Tc$}
          %  % \doubleLine
          %  % \UnaryInfC{$S_1 \seq (S_2 \seq T)$}
          %  \DisplayProof
\qquad\qquad\qquad\qquad
           % \AxiomC{$(\Sc \seq \Tc_2) \seq \Tc_1$}
           % \doubleLine
           % \UnaryInfC{$\Sc \seq (\Tc_1 , \Tc_2)$}
           % % \doubleLine
           % % \UnaryInfC{$(S \seq T_1) \seq T_2$}
           % \DisplayProof
% \quad
           \AxiomC{$Z_a < Y_s \sequent X_s$}
           \doubleLine
           \UnaryInfC{$Z_a \sequent X_s , Y_s$}
           \doubleLine
           \UnaryInfC{$Z_a < X_s \sequent Y_s$}
           \DisplayProof
   \]

% To go back, compute whether a given $\seq$ is an
% ``antecedent'' or ``succedent'' part, and replace it with $<$ or $>$
% as appropriate.

% \vfill
%  \item[Display Property:] For every positive (negative) context
%    $X[~]$ and every $\Sc$, there exists $\Tc$ such that $\Tc \seq
%    \Sc$ (respectively $\Sc \seq \Tc$) is derivable from $X[\Sc]$ using
%    only the structural turn rules above.
% %from $\{ \drp_1, drp_2, \rp_1, rp_2\}.$
%    Thus $\Sc$ is ``displayed'' in $\Tc\seq\Sc$ (resp.\  $\Sc\seq\Tc$).
%  \item[Polarity:] note that $\seq$ always points to the positive contexts
  \end{description}
\end{frame}

\begin{frame}
  \frametitle{Nested sequent calculi: Kashima 1994 (for tense logics)}

  \begin{description}[M]
 \item[Nested sequent:] where comma is associative and commutative
  $$
  S~~T \;::=\; S_1,\dots,S_k,A_1,\dots,A_m \seq B_1,\dots, B_n, T_1, \dots,T_l
  $$

\item[Context:] nested sequent with exactly one hole $[~]$
\item[Positive/Negative:] if $[~]$ occurs immediately to 
  right/left of $\seq$


%\vfill
% \item[Shallow nested sequent calculus:] Notational variant of display
%   calculi where all occurrences of $\turn$ and $<$ and $>$ are
%   replaced by $\seq$ and associativity and commutativity of comma are
%   built-in

\vfill
\item[Turn Rules:] reversible rules using \textbf{multisets} of 
     nested sequents and formulae
   \[
% \hspace*{-1cm}
%           \AxiomC{$X_a \sequent Y_a > Z_s$}
%            \doubleLine
%            \UnaryInfC{$X_a , Y_a \sequent Z_s$}
%            \doubleLine
%            \UnaryInfC{$Y_a \sequent X_a > Z_s$}
%            \DisplayProof
% \quad
          \AxiomC{$\Sc_2 \seq (\Sc_1 \seq \Tc)$}
           \doubleLine
           \UnaryInfC{$\Sc_1 , \Sc_2 \seq \Tc$}
           % \doubleLine
           % \UnaryInfC{$S_1 \seq (S_2 \seq T)$}
           \DisplayProof
\qquad\qquad\qquad\qquad
           \AxiomC{$(\Sc \seq \Tc_2) \seq \Tc_1$}
           \doubleLine
           \UnaryInfC{$\Sc \seq (\Tc_1 , \Tc_2)$}
           % \doubleLine
           % \UnaryInfC{$(S \seq T_1) \seq T_2$}
           \DisplayProof
% \quad
%            \AxiomC{$Z_a < Y_s \sequent X_s$}
%            \doubleLine
%            \UnaryInfC{$Z_a \sequent X_s , Y_s$}
%            \doubleLine
%            \UnaryInfC{$Z_a < X_s \sequent Y_s$}
%            \DisplayProof
   \]

% To go back, compute whether a given $\seq$ is an
% ``antecedent'' or ``succedent'' part, and replace it with $<$ or $>$
% as appropriate.

\vfill
 \item[Display Property:] For every positive (negative) context
   $X[~]$ and every $\Sc$, there exists $\Tc$ such that $\Tc \seq
   \Sc$ (respectively $\Sc \seq \Tc$) is derivable from $X[\Sc]$ using
   only the structural turn rules above.
%from $\{ \drp_1, drp_2, \rp_1, rp_2\}.$
   Thus $\Sc$ is ``displayed'' in $\Tc\seq\Sc$ (resp.\  $\Sc\seq\Tc$).
 \item[Polarity:] note that $\seq$ always points to the positive contexts
  \end{description}
\end{frame}

\begin{frame}
  \frametitle{Shallow nested sequent calculus for $\biill$}
  
\tblue{Logical rules:}
\vfill
{\small
  \begin{tabular}[c]{l@{\extracolsep{2cm}}l}
$
\qquad
\vcenter{
\infer[id]
{p \seq p}{}
}
$
&
$
\vcenter{
\infer[cut]
{\Sc,\Tc \seq \Sc', \Tc'}
{\Sc \seq \Sc', A & A, \Tc \seq \Tc'}
}
$
\\[15px]
\multicolumn{2}{c}{
$
 \infer[\punit_l]
{\punit \seq \sunit}
{}
\qquad
\infer[\punit_r]
{\Sc \seq \Tc, \punit}
{\Sc \seq \Tc}
\qquad
\infer[\tunit_l]
{\Sc, \tunit \seq \Tc}
{\Sc \seq \Tc}
\qquad
\infer[\tunit_r]
{\sunit \seq \tunit}{}
$
}
\\[12px]
$
\infer[\ltens_l]
{\Sc, A \ltens B \seq \Tc}
{\Sc, A, B \seq \Tc}
$
&
$\infer[\ltens_r]
{\Sc, \Sc' \seq A \ltens B, \Tc, \Tc'}
{\Sc \seq A, \Tc & \Sc' \seq B, \Tc'}
$
\\[12px]
$
\infer[\parr_l]
{\Sc, \Sc', A \parr B \seq \Tc, \Tc'}
{\Sc, A \seq \Tc & \Sc', B \seq \Tc'}
$
&
$
\infer[\parr_r]
{\Sc \seq A \parr B, \Tc}
{\Sc \seq A, B, \Tc}
$
\\[12px]
$
\infer[\limp_l]
{\Sc, \Sc', A \limp B \seq \Tc, \Tc'}
{
\Sc \seq A, \Tc
&
\Sc', B \seq \Tc'
}
$
&
$
\infer[\limp_r]
{\Sc \seq \Tc, A \limp B}
{\Sc \seq \Tc, (A \seq B)}
$
\\[12px]
$
\infer[\excl_l]
{\Sc, A \excl B \seq \Tc}
{
 \Sc, (A \seq B) \seq \Tc
}
$
&
$
\infer[\excl_r]
{\Sc, \Sc' \seq A \excl B, \Tc, \Tc'}
{
 \Sc \seq A, \Tc & 
 \Sc', B \seq \Tc'
}
$
 \end{tabular}
}

\end{frame}

\begin{frame}
  \frametitle{Shallow nested sequent calculus for $\biill$}

  \begin{description}[M]
  \item[Structural Rules:] Grishin (b) analogues
\\[12px]
  \begin{tabular}[c]{l@{\extracolsep{2cm}}l}
      \mbox{$\infer[gl]
           {(\Sc, \Tc \seq \Sc') \seq \Tc'}
           {\Tc , (\Sc \seq \Sc') \seq \Tc'}
           $} 
&
      \mbox{$\infer[gr]
             {\Sc \seq (\Sc' \seq \Tc', \Tc)}
             {\Sc \seq (\Sc' \seq \Tc'), \Tc}
           $}
 \end{tabular}

\vfill

  \begin{tabular}[c]{l@{\extracolsep{0.5cm}}l}
{\small
  \AxiomC{$W,(X<Y)\turn Z$}
    \LeftLabel{(Grnb $\turn$)}
  \UnaryInfC{$(W,X)<Y\turn Z$}
  \DisplayProof
}
  &
{\small
  \AxiomC{$W\vdash (X> Y), Z$}
    \LeftLabel{($\turn$ Grnb)}
  \UnaryInfC{$W\vdash X>(Y,Z)$}
  \DisplayProof
}
 \end{tabular}

\vfill
  \item[Thm:] Every formula has a cut-free nested shallow sequent derivation
    iff it has cut-free display calculus derivation

\item[Thm:] if a nested sequent 
%$X$ $\Sc \seq \Tc$ 
is derivable it is cut-free derivable
\item[Proof:] essentially the same as for display calculus
\vfill
\item[Prof search:] how to absorb the turn and $gl$ and
  $gr$ rules~?
  \end{description}
\end{frame}

\begin{frame}
  \frametitle{Deep nested sequents: just apply the rules inside
    contexts}

{\small
\hspace*{-0.5cm}
  \begin{tabular}[c]{ll}
$
\infer[id^d]
{X[\Uc, p \seq p, \Vc]}
{\mbox{$X[~]$ and $\Uc$ and $\Vc$ are hollow.}}
$& 
\raisebox{0.3cm}{similarly for units (no cut rule)}
% \\[12px]
% $
% \infer[\punit_l^d]
% {X[\punit, \Uc \seq \Vc]}
% {\mbox{$X[~]$, $\Uc$ and $\Vc$ are hollow. }}
% $&$
% \infer[\punit_r^d]
% {X[\Sc \seq \Tc, \punit]}
% {X[\Sc \seq \Tc]}
% $
% \\[12px]
% $
% \infer[\tunit_l^d]
% {X[\Sc, \tunit \seq \Tc]}
% {X[\Sc \seq \Tc]}
% $&$
% \infer[\tunit_r^d]
% {X[\Uc \seq \tunit, \Vc]}
% {\mbox{$X[~]$, $\Uc$ and $\Vc$ are hollow. }}
% $
\\[12px]
$
\infer[\ltens_l^d]
{X[\Sc, A \ltens B \seq \Tc]}
{X[\Sc, A, B \seq \Tc]}
$&$
\infer[\ltens_r^d]
{X[\Sc \seq A \ltens B, \Tc]}
{X_1[\Sc_1 \seq A, \Tc_1] & X_2[\Sc_2 \seq B, \Tc_2]}
$
\\[12px]
$\infer[\limp_l^d]
{X[\Sc, A \limp B \seq \Tc]}
{
X_1[\Sc_1 \seq A, \Tc_1] & X_2[\Sc_2, B \seq \Tc_2]
}
$&$
\infer[\limp_r^d]
{X[\Sc \seq \Tc, A \limp B]}
{X[\Sc \seq \Tc, (A \seq B)]}
$
\\[12px]
$
\infer[\parr_l^d]
{X[\Sc, A \parr B \seq \Tc]}
{
 X_1[\Sc_1, A \seq \Tc_1]
 &
 X_2[\Sc_2, B \seq \Tc_2]
}
$&$
\infer[\parr_r^d]
{X[\Sc \seq A \parr B, \Tc]}
{X[\Sc \seq A, B, \Tc]}
$
\\[12px]
$
\infer[\excl_l^d]
{X[\Sc, A \excl B \seq \Tc]}
{X[\Sc, (A \seq B) \seq \Tc]}
$&$
\infer[\excl_r^d]
{X[\Sc \seq A \excl B, \Tc]}
{X_1[\Sc_1 \seq A, \Tc_1] 
&
 X_2[\Sc_2, B \seq \Tc_2]
}
$
  \end{tabular}
}

\vfill

\begin{description}[M]
  \item[Hollow:] $X[]$ contains no formulae ($\seq$-tree of
    empty nodes)
  \item[Merge:] $X[~] \in X_1[~] \merge X_2[~]$ and
  $\Sc \in \Sc_1 \merge \Sc_2$ and $\Tc \in \Tc_1 \merge \Tc_2$
\end{description}

\end{frame}

\begin{frame}
  \frametitle{Deep nested sequents: just apply the rules inside contexts}

  \begin{description}[M]
  \item[Propagation rules:] allow formulae to be moved in a context
\\[12px]
{\small
  \begin{tabular}[c]{ll}
$
\infer[pl_1]
{X[\Sc, A \seq (\Sc' \seq \Tc'), \Tc]}
{
 X[\Sc \seq (\Sc',A  \seq \Tc'), \Tc]
}
$
&
$\infer[pr_1]
{X[\Sc', (\Sc \seq \Tc) \seq A, \Tc']}
{X[\Sc', (\Sc \seq A, \Tc) \seq \Tc']}
$
\\[12px]
$
\infer[pl_2]
{X[\Sc, (\Sc', A \seq \Tc') \seq \Tc]}
{X[\Sc, (\Sc' \seq \Tc'), A \seq \Tc]}
$&$
\infer[pr_2]
{X[\Sc \seq (\Sc' \seq A, \Tc'), \Tc]}
{X[\Sc \seq A, (\Sc' \seq \Tc'), \Tc]}
$
  \end{tabular}
}

\vfill
\item[Note:] these are not just reversible rules expanded into two!
\item[Note:] the rules do not need to track polarity

\pause
\vfill
\item[Thm:] the turn rules and rules $gl$ and $gr$ are (cut-free) admissible

\item[Thm:] if a nested sequent is (cut-free) derivable in the deep
  calculus then it is cut-free derivable in the shallow calculus
% \item[Proof:] every deep rule is cut-free
%   derivable in the shallow calculus
\item[Thm:] if a nested sequent is cut-free derivable in the shallow
  calculus then it is (cut-free) derivable in the deep calculus
% \item[Proof:] add structural rules to the deep calculus and show
%   they permute up to the leaves, where they become
%   redundant 
\item[Cor:] the deep and shallow nested calculi derive the same sequents

  \end{description}

\end{frame}

\begin{frame}{From $\biill$ back to $\fill$}

{\small
\AxiomC{$a\turn a$}
\AxiomC{$b\turn b$}%\LeftLabel{\scriptsize{($\parr\turn$)}}
\BinaryInfC{$a\tgreen{\;\parr\;} b\turn a,b$}
\AxiomC{$c\turn c$}%\LeftLabel{\scriptsize{($\parr\turn$)}}
\BinaryInfC{$(a\parr b)\tred{\;\parr\;} c \turn \tblue{(a,b)},c$}% \LeftLabel{\scriptsize{\textbf{(?)}}}
\UnaryInfC{$(a\parr b)\parr c \turn a,(b,c)$} \LeftLabel{\scriptsize{\textbf{(?)}}}
\UnaryInfC{$(a\parr b)\parr c\tred{\;<\;}a \turn \tblue{b,c}$} \LeftLabel{\scriptsize{($\turn\parr$)}}
\UnaryInfC{$(a\parr b)\parr c<a\turn \tblue{b\parr c}$}
\AxiomC{$d\turn d$}\LeftLabel{\scriptsize{($\limp\turn$)}}
\BinaryInfC{$b \parr c \tred{\;\limp\;} d \turn ((a\parr b)\parr c<a)\tred{\;>\;}d$}
\AxiomC{$e\turn e$}\LeftLabel{\scriptsize{($\parr\turn$)}}
\BinaryInfC{$(b\parr c\limp d)\tgreen{\;\parr\;} e \turn \tblue{(}((a\parr b)\parr c<a)>d\tblue{)},e$}\LeftLabel{\scriptsize{\tblue{(?)}}}
\UnaryInfC{$(b\parr c\limp d)\parr e \turn ((a\parr b)\parr c<a)\tred{\;>\;}(d,e)$}\LeftLabel{\scriptsize{(?)}}
\UnaryInfC{$(b\parr c\limp d)\parr e\tred{,}((a\parr b)\parr c<a)\turn \tblue{d,e}$}\LeftLabel{\scriptsize{($\turn\parr$)}}
\UnaryInfC{$\tgreen{(b\parr c\limp d)\parr e},((a\parr b)\parr c<a)\turn \tblue{d\parr e}$}\LeftLabel{\scriptsize{(?)}}
\UnaryInfC{$(a\parr b)\parr c<a \turn \tgreen{(b\parr c\limp d)\parr e}\tred{\;>\;}(d\parr e)$}\LeftLabel{\scriptsize{\tblue{($\turn\limp$)}}}
\UnaryInfC{$(a\parr b)\parr c\tblue{\;<a} \turn (b\parr c\limp d)\parr e\tred{\;\limp\;} (d\parr e)$}\LeftLabel{\scriptsize{\textbf{(?)}}}
\UnaryInfC{$(a\parr b)\parr c \turn \tblue{a,}(b\parr c\limp d)\parr e\limp (d\parr e)$}
\DisplayProof
}


\end{frame}


\begin{frame}
  \frametitle{From $\biill$ back to $\fill$}

  \begin{description}[M]
  \item[Problem:] all our calculi are for $\biill$ ... are they sound
    for $\fill$?
  \item[Display calculus:] must create antecedent $<$ structures in
    its derivation of $\fill$-formulae in order to display and
    undisplay
  \item[Question:] is $\biill$ a conservative extension of $\fill$?

\pause
\vfill
  \item we were not able to find a categorial proof for $\biill$
\vfill
   \item[Compare:] to tense logic Kt say where there is a simple
      semantic proof that Kt is a conservative extension of K (same frames)
  \end{description}

\end{frame}

\begin{frame}
  \frametitle{From $\biill$ back to $\fill$}

  \begin{description}[M]
  \item[Nested $\fill$-sequent:] nested sequent that has no nesting of
    sequents on the left of $\seq$ and no occurrences of $\excl$
  \item[Why?] because then it is free of any traces of $\excl$ since
    only the $\excl^d_l$ rule creates such nestings

\vfill
  \item[$\fill_{dn}$:] remove $\excl^d_{l}$, $\excl^d_{r}$, $pl_2$ and $pr_1$ 

\pause
\vfill
  \item[Separation Thm:] nested FILL-sequents are (cut-free) derivable
    in $\fill_{dn}$ iff they are derivable in the original deep calculus
  \item[Proof:] if the end-sequent contains only $\fill$-formulae then
    backward proof search will never create the offending nesting
  \item[Thm:] every rule of $\fill_{dn}$ preserves $\fill$-validity
    downwards
  \item[Cor:] $\fill_{dn}$ is sound and cut-free complete for $\fill$-validity
  % \item[Cor:] A $\fill$-formulae is $\fill$-valid iff it is (cut-free)
  %   $\fill_{dn}$-derivable 
%and $\biill$ is a conservative extension of $\fill$
  \item[Cor:] 
    % A $\fill$-formulae is $\fill$-valid iff it is (cut-free)
    % derivable in $\fill_{dn}$ and 
    $\biill$ is a conservative extension of $\fill$
  \end{description}

\end{frame}

\begin{frame}
  \frametitle{Complexity of deciding $\fill$}

  \begin{description}[M]
    \item[Backward proof search:] need to try all ways to partition a
      context and apply all propagation rules in all ways, but this
      terminates
    \item[Subformula property:] every formula in the premises is a
      subformula of a formula in the conclusion
    \item[Complexity: ] $\fill$ is in NP
    \item[Proof:] guess a cut-free derivation and check it in time polynomial in
      size of the given formula. Possible since each formula is
      introduced exactly once in any derivation
    \item[Complexity:] our calculus handles the problem of deciding
      constants-only multiplicative linear logic (COMLL) since the
      nnf-formulae of this logic contain no propositional atoms and no
      implication connectives and it is known to be
      NP-hard
    \item[Thm:] deciding $\fill$-validity is NP-complete
  \end{description}
\end{frame}

\begin{frame}{Our Methodology}

  \begin{description}[M]
  \item[Start] with a categorially formulated logic $L$
    \item[Give] a \Tcg{display calculus} for $L$
    \begin{description}[M]
      \item[$\tcg{\checkmark}$]
      Easily shown to be complete.
      \item[$\tcg{\checkmark}$]
      Easily shown to support a cut-elimination procedure.
      \item[\mbox{\tcr{X}}]
      Embeds $L$ into an extension so conservativity, and hence
      soundness, not clear.
      \item[\mbox{\tcr{X}}]
      Not well suited for proof search.
    \end{description}
  \item[Refine] to a \Tcg{nested sequent calculus}
    with \Tcg{deep inference}.
    \begin{description}[M]
      \item[$\tcg{\checkmark}$]
      Conservativity, and hence soundness, now clear.
      \item[$\tcg{\checkmark}$]
      Supports proof search and complexity analysis.
    \end{description}
  \item[Question:] how far can we push this methodology?

\pause
\vfill
  \item[We know:] it works for the exponentials $\bang$ and $\gnab$
  \item[But:] $\biill$ plus additives not conservative over $\fill$
    plus additivies e.g $\top \vdash p, \top$ is $\biill$-valid but
    not $\fill$-valid
%  \item Any help appreciated!
  \end{description}

\end{frame}

\begin{frame}
  Happy (belated) birthday Gerhard!
\end{frame}

\begin{frame}{Belnap's Eight Conditions a l\'a Kracht}
\small

\begin{description}[M]
\item[(C1)] Each formula variable occurring in some premise of a rule $\rho$ is a subformula
of some formula in the conclusion of~$\rho$.
\item[(C2)] \textit{Congruent parameters} is a relation between parameters of the identical structure variable occurring 
in the premise and conclusion 
%sequents. 
\item[(C3)] Each parameter is congruent to at most one structure variable in the conclusion. Equivalently,
no two structure variables in the conclusion are congruent to each other.
\item[(C4)] Congruent parameters are either all antecedent or all succedent parts of their respective sequent.
\item[(C5)] A formula in the conclusion of a rule~$\rho$ is either the entire
antecedent or the entire succedent. 
Such a formula is called a \textbf{principal formula} of~$\rho$.
\item[(C6/7)] Each rule is closed under simultaneous substitution of arbitrary structures for congruent
parameters.
\end{description}

\end{frame}

\begin{frame}{Belnap's Eight Conditions a l\'a Kracht}
\small

\begin{description}[M]
\item[(C8)] If there are rules $\rho$ and $\sigma$ with respective
conclusions $X\turn A$ and $A\turn Y$ with formula $A$ principal in
both inferences (in the sense of C5) and if $cut$ is applied to
yield $X\turn Y$, then either $X\turn Y$ is identical to either
$X\turn A$ or $A\turn Y$; or it is possible to pass from the
premises of $\rho$ and $\sigma$ to $X\turn Y$ by means of inferences
falling under $cut$ where the cut-formula always is a proper
subformula of $A$. 
\end{description}

\AxiomC{$X \vdash C > D$}
\UnaryInfC{$X \vdash C \mlim D$}
\AxiomC{$U \vdash C$}
\AxiomC{$D \vdash Z$}
\BinaryInfC{$C \mlim D \vdash U > Z$}
\RightLabel{cut}
\BinaryInfC{$X \vdash U > Z$}
\DisplayProof

\bigskip


\hfill
\AxiomC{$U \vdash C$}
\AxiomC{$X \vdash C > D$}
\UnaryInfC{$X, C \vdash D$}
\AxiomC{$D \vdash Z$}
\RightLabel{cut}
\BinaryInfC{$X,C \vdash Z$}
\UnaryInfC{$C \vdash X > Z$}
\RightLabel{cut}
\BinaryInfC{$U \vdash X > Z$}
\UnaryInfC{$X, U \vdash Z$}
\UnaryInfC{$X \vdash U > Z$}
\DisplayProof

\end{frame}

\begin{frame}
  \frametitle{Devil's Advocate Questions}

% Why can't we just add Grishin rules to the original sequent calculus
% using $\Gamma \vdash \Delta$? 

% \begin{tabular}[c]{ll}
% \raisebox{0.5cm}{$((A \mlim B) \parr C) \mlim (A \mlim (B \parr C))$}
% % &
% % {\small
% % $\infer[pr_2]
% % {X[\Sc \seq (\Sc' \seq A, \Tc'), \Tc]}
% % {X[\Sc \seq A, (\Sc' \seq \Tc'), \Tc]}
% % $
% % }
% % \\[12px]
% % {\small
% %   \AxiomC{$W\vdash (X> Y), Z$}
% %     \LeftLabel{($\turn$ Grnb)}
% %   \UnaryInfC{$W\vdash X>(Y,Z)$}
% %   \DisplayProof
% % }
% &
% \AxiomC{$\Gamma , A \vdash B , C, \Delta$}
% \UnaryInfC{$\Gamma \vdash (A \mlim B) , C, \Delta$}
% \UnaryInfC{$\Gamma \vdash (A \mlim B) \parr C, \Delta$}
% \UnaryInfC{$\Gamma \vdash A \mlim (B \parr C), \Delta$}
% \DisplayProof
% \end{tabular}
% \vfill
% Cut-elimination will fail since we can write complex formulae which
% imply $((A \mlim B) \parr C)$ but never actually contain it as such.

Can't we do all of this with labelled sequent calculi?
\[
\AxiomC{$\Gamma , R(x,y,z), x:A \vdash z:B , \Delta$}
\RightLabel{$x$ and $y$ do not occur in the conclusion}
\UnaryInfC{$\Gamma \vdash y:(A \mlim B) , \Delta$}
\DisplayProof
\]

Almost certainly we can, but the decidability cannot be read off as we
are able to do, and I can't see the ``Grishin'' condition
  

\vfill

Where are the Grishin rules in the deep calculus? 

In the logical rules and propagation rules 

{\small
$$
\infer[\parr_l^d]
{X[\Sc, A \parr B \seq \Tc]}
{
 X_1[\Sc_1, A \seq \Tc_1]
 &
 X_2[\Sc_2, B \seq \Tc_2]
}
\qquad
\infer[pr_2]
{X[\Sc \seq (\Sc' \seq A, \Tc'), \Tc]}
{X[\Sc \seq A, (\Sc' \seq \Tc'), \Tc]}
$$
}

\vfill

Isn't ``merge'' just another way of hiding annotations? No, it is a
very natural definition ... superpose two identical $\seq$-trees 
\end{frame}


\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 