\documentclass{lecture}

\usepackage{amsmath}
\usepackage{latexsym}
\usepackage{amssymb}
%\usepackage{proof}
\usepackage{exptrees}

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{definition}{Definition}

\newcommand{\pordered}[3]{#1 <_{\texttt{\scriptsize #2}} #3}
\newcommand{\LRPord}[2]{\pordered{#1}{LRP}{#2}}
\newcommand{\cutord}[2]{\pordered{#1}{cut}{#2}}
\newcommand{\snoneord}[2]{\pordered{#1}{sn1}{#2}}
\newcommand{\dtord}[2]{\pordered{#1}{dt}{#2}}

%\input{/home/discus/disk1/rpg/papers/relalg/csl96/defs}

\newcommand{\comment}[1]{}
\newcommand{\mytilde}{\scriptstyle\sim}

\newcommand\vpf{\vspace{-3ex}} % to reduce space before proof tree

%%%%% Rule Forming Commands

\newcommand{\idrule}[2]{
 \mbox{#1 \ $\mbox{#2}$}}

\newcommand{\ds}{\displaystyle\strut}

\newcommand{\urule}[3]{
 \mbox{#1 \ $\frac{\ds \mbox{#2}}{\ds \mbox{#3}}$}}


\newcommand{\brule}[4]{
 \mbox{#1 \ $\frac{\ds \mbox{#2}\ \ \ \ \mbox{#3}}
                   {\ds \mbox{#4}}$}}


\newcommand\invrule[3]{
\begin{tabular}{r@{}l}
 \multicolumn{1}{r}{#1} & 
 \begin{tabular}{@{}c@{}}
     \raisebox{0.2em}{#2} 
     \\ \hline \hline 
     \raisebox{-0.2em}{#3} 
 \end{tabular}
\end{tabular}
}

\newcommand\doubleinvrule[4]{
\begin{tabular}{r@{}l}
 \multicolumn{1}{r}{#1} & 
 \begin{tabular}{@{}c@{}}
     #2 \\[0.4em] \hline \hline 
     \raisebox{-0.4em}{#3} \\[0.7em] \hline \hline 
     \raisebox{-0.4em}{#4} 
 \end{tabular}
\end{tabular}
}

\newcommand{\Drel}{\mbox{\bf DRA }}
\newcommand{\Lg}[1]{\mbox{$\bf #1$}}

\newcommand{\Fml}{\mbox{$\mathbf{Fml}$}}
\newcommand{\LAlg}{\mbox{$\mathfrak{Fml}/\!\!\equiv$}}

\newcommand{\stc}{\bullet}

\newcommand{\blob}{\bullet}

\newcommand{\mcyl}{\raisebox{0.2ex}{\bf c}}
\newcommand{\mor}{+}
\newcommand{\mand}{\circ}
\newcommand{\mnot}{\sim}
\newcommand{\mimp}{\rightarrow}
\newcommand{\mif}{\leftarrow}
\newcommand{\mtop}{\mbox{\bf 1}}
\newcommand{\mbot}{\mbox{\bf 0}}
%\newcommand{\myzero}{\mbox{\bf 0}}
\newcommand{\mstar}{\bigstar}

\newcommand{\mcal}[1]{\mbox{$\cal #1$}}

\newcommand{\btop}{\top}
\newcommand{\bbot}{\bot}
\newcommand{\bor}{\vee}
\newcommand{\band}{\wedge}
\newcommand{\bnot}{\neg}
\newcommand{\bimp}{\supset}

\newcommand{\conv}{\smallsmile}
\newcommand{\semic}{\mbox{ ; }}
\newcommand{\comma}{\raisebox{0.5ex}{ , }}
%\newcommand{\colon}{\mbox{ : }}
\newcommand{\myE}{ E }

\newcommand{\Dl}[1]{\mbox{$\bf \mathbf{\delta}#1$}}
\newcommand{\eqded}{\dashv \vdash}

\newcommand{\AstLeft}{
 \invrule{ }{$\ast X \vdash Y$}{$\ast Y \vdash X$}
}

\newcommand{\AstRight}{
 \invrule{ }{$X \vdash \ast Y$}{$Y \vdash \ast X$}
}

\newcommand{\AstAstLeft}{
 \invrule{ }{$\ast \ast X \vdash Y$}{$X \vdash Y$}
}

\newcommand{\AstAstRight}{
 \invrule{ }{$X \vdash \ast \ast Y$}{$X \vdash Y$}
}

\newcommand{\ResidConv}{
 \invrule{ }{$\stc X \vdash Y$}{$X \vdash \stc Y$}
}

\newcommand{\ConvConvLeft}{
 \invrule{ }{$\stc \stc X \vdash Y$}{$X \vdash Y$}
}

\newcommand{\ConvConvRight}{
 \invrule{ }{$X \vdash \stc \stc Y$}{$X \vdash Y$}
}

\newcommand{\ConvAstLeft}{
 \invrule{ }{$\stc \ast X \vdash Y$}{$\ast \stc X \vdash Y$}
}

\newcommand{\PTwoAstConvLeft}{
 \invrule{ }{$X \vdash Y$}{$\ast \stc \ast \stc X \vdash Y$}
}

\newcommand{\PTwoAstConvRight}{
 \invrule{ }{$Y \vdash X $}{$Y \vdash \ast \stc \ast \stc X $}
}

\newcommand{\ConvAstRight}{
 \invrule{ }{$X \vdash \stc \ast Y$}{$X \vdash \ast \stc Y$}
}

\newcommand{\ResidTwoLeft}{
 \doubleinvrule{ }{$X \vdash \ast (\ast Z \semic \stc Y)$}
                  {$X \semic Y \vdash Z$}
                  {$Y \vdash \ast (\stc X \semic \ast Z)$}
}

\newcommand{\ResidTwoRight}{
 \doubleinvrule{ }{$\ast (\ast Z \semic \stc Y) \vdash X $}
                  {$Y \vdash Z \semic X $}
                  {$\ast (\stc X \semic \ast Z) \vdash Y $}
}

\newcommand{\ResidOneLeft}{
 \doubleinvrule{ }{$X \vdash \ast \stc (Y \semic \ast \stc Z)$}
                  {$X \semic Y \vdash Z$}
                  {$Y \vdash \ast \stc (\ast \stc  Z \semic X)$}
}

\newcommand{\ResidOneRight}{
 \doubleinvrule{ }{$\ast \stc (Y \semic \ast \stc Z) \vdash X $}
                  {$Z \vdash X \semic Y$}
                  {$\ast \stc (\ast \stc  Z \semic X) \vdash Y $}
}

\newcommand{\dpcircleRight}{
 \doubleinvrule{ }{$\ast (\ast Z \semic \stc Y) \vdash X $}
                  {$Z \vdash X \semic Y$}
                  {$\ast (\stc X \semic \ast Z) \vdash Y $}
}

\newcommand{\DualResidInt}{
 \doubleinvrule{ }{$Z \semic \ast \stc Y \vdash X$}
                  {$Z \vdash X \semic Y$}
                  {$\ast \stc X \semic Z \vdash Y$}
}

\newcommand{\ResidInt}{
 \doubleinvrule{ }{$X \vdash Z \semic \ast \stc Y$}
                  {$X \semic Y \vdash Z$}
                  {$Y \vdash \ast \stc X \semic Z$}
}

\newcommand{\DualResidExt}{
 \doubleinvrule{ }{$Z \comma \vphantom{\semic} \ast Y \vdash X$}
                  {$Z \vdash X \vphantom{\semic} \comma Y$}
                  {$\ast X \comma \vphantom{\semic} Z \vdash Y\,\,\,$}
}

\newcommand{\ResidExt}{
 \doubleinvrule{ }{$X \vdash Z \vphantom{\semic} \comma \ast Y$}
                  {$X \comma Y \vphantom{\semic} \vdash Z$}
                  {$Y \vdash \ast X \vphantom{\semic} \comma Z \,\,\,$}
}

\newcommand{\ConvDistrLeft}{
 \invrule{ }{$\stc (X \semic Y) \vdash Z$}
            {$(\stc Y) \semic (\stc X) \vdash Z$}
}

\newcommand{\ConvDistrRight}{
 \invrule{ }{$Z \vdash \stc (X \semic Y) $}
            {$Z \vdash (\stc Y) \semic (\stc X) $}
}


\newcommand{\dpstccircRight}{
 \invrule{ }{$Z \vdash \stc (X \semic Y) $}
            {$Z \vdash (\stc Y) \semic (\stc X) $}
}

\newcommand{\Tagging}{
 \urule{(tag)}{$X \semic Y \vdash Z $}
            {$\stc Y \semic \stc X \vdash \stc Z$}
}

\newcommand{\TagInvLeft}{
 \urule{$(taginv \vdash)$}{$\stc Y \semic \stc X \vdash \stc Z$}
              {$X \semic Y \vdash Z $}
}            

\newcommand{\TagInvRight}{
 \urule{$(\vdash taginv)$}{$\stc Z \vdash \stc Y \semic \stc X $}
              {$Y \vdash Z \semic X $}
}            

\newcommand{\ConvmyELeft}{
 \invrule{($\stc \myE \vdash$)}{$\myE \vdash X$}
            {$\stc \myE \vdash X$}
}

\newcommand{\ConvmyERight}{
 \invrule{($\vdash \stc \myE$)}{$X \vdash \myE$}
            {$X \vdash \stc \myE$}
}

\newcommand{\ConvTopLeft}{
 \invrule{($\stc I \vdash$)}{$I \vdash X$}
            {$\stc I \vdash X$}
}

\newcommand{\ConvTopRight}{
 \invrule{($\vdash \stc I$)}{$X \vdash I$}
            {$X \vdash \stc I$}
}

\newcommand{\CommaAssLeft}{
 \invrule{($A \vdash$)}{$X \comma  (Y  \comma  Z) \vdash W$}
            {$(X  \comma  Y) \comma  Z \vdash W$}
}

\newcommand{\CommaAssRight}{
 \invrule{($\vdash A$)}{$W \vdash X \comma  (Y  \comma  Z)$}
            {$W \vdash (X  \comma  Y) \comma  Z $}
}

\newcommand{\SemicAssLeft}{
 \invrule{($A \semic \vdash$)}{$X \semic  (Y  \semic  Z) \vdash W$}
            {$(X  \semic  Y) \semic  Z \vdash W$}
}

\newcommand{\SemicAssRight}{
 \invrule{($\vdash A \semic$)}{$W \vdash X \semic  (Y  \semic  Z)$}
            {$W \vdash (X  \semic  Y) \semic  Z $}
}

\newcommand{\CommaComLeft}{
 \urule{($P \vdash$)}{$Y  \comma  X \vdash Z $}
            {$X  \comma  Y \vdash Z $}
}

\newcommand{\CommaComRight}{
 \urule{($\vdash P$)}{$Z \vdash Y  \comma  X $}
            {$Z \vdash X  \comma  Y $}
}

\newcommand{\CommaContLeft}{
 \urule{($C \vdash$)}{$X  \comma  X \vdash Z $}
            {$X  \vdash Z $}
}

\newcommand{\CommaContRight}{
 \urule{($\vdash C$)}{$Z \vdash X  \comma  X $}
            {$Z \vdash X $}
}

\newcommand{\CommaWeakLeft}{
 \urule{($M \vdash$)}{$X \vdash Z $}
            {$X  \comma  Y \vdash Z $}
}

\newcommand{\CommaWeakRight}{
 \urule{($\vdash M$)}{$Z \vdash X $}
            {$Z \vdash X \comma  Y$}
}


\newcommand{\AntiLogLeft}{
 \invrule{$(alg \vdash)$}{$X \semic Y \vdash Z $}
            {$\ast \stc Z \semic X \vdash \ast \stc Y$}
}

\newcommand{\AntiLogRight}{
 \invrule{$(\vdash alg)$}{$Z \vdash X \semic Y $}
            {$\ast \stc Y \vdash \ast \stc Z \semic X $}
}

\newcommand{\myEPlusMinusLeft}{
 \doubleinvrule{$(\myE^{+}_{-} \vdash)$}
               {$X \semic \myE \vdash Y$}
               {$X \vphantom{\semic} \vdash Y $}
               {$\myE \semic X \vdash Y$}
}

\newcommand{\myEPlusMinusRight}{
 \doubleinvrule{$(\vdash \myE^{+}_{-})$}
               {$X \vdash \myE \semic Y $}
               {$X \vphantom{\semic} \vdash Y $}
               {$X \vdash Y \semic \myE $}
}


\newcommand{\IPlusMinusLeft}{
 \doubleinvrule{$(I^{+}_{-} \vdash)$}
               {$X \comma I \vdash Y$}
               {$X \vdash Y $}
               {$I \comma X \vdash Y$}
}

\newcommand{\IPlusMinusRight}{
 \doubleinvrule{$(\vdash I^{+}_{-} )$}
               {$X \vdash I \comma Y $}
               {$X \vdash Y $}
               {$X \vdash Y \comma I $}
}


\newcommand{\ExI}{
 \urule{(ExI)}
          {$X \vdash I$}
          {$X \vdash Y$}
}

\newcommand{\VerI}{
 \urule{(VerI)}
          {$I \vdash X$}
          {$Y \vdash X$}
}

\newcommand{\mtopLeft}{
 \urule{$(\mtop \vdash)$}
          {$\myE \vdash Z $}
          {$\mtop \vdash Z$}
}

\newcommand{\mtopRight}{
 \idrule{$(\vdash \mtop)$}{$E \vdash \mtop$}
}

\newcommand{\mbotRight}{
 \urule{$(\vdash \mbot)$}
          {$Z \vdash \myE $}
          {$Z \vdash \mbot$}
}

\newcommand{\mbotLeft}{
 \idrule{$(\mbot \vdash)$}{$\mbot \vdash E $}
}

\newcommand{\mnotLeft}{
 \urule{$(\mnot \vdash)$}
          {$\ast \stc A \vdash Z $}
          {$\mnot A \vdash Z$}
}

\newcommand{\mnotRight}{
 \urule{$(\vdash \mnot)$}
          {$Z \vdash \ast \stc A $}
          {$Z \vdash \mnot A $}
}

\newcommand{\convLeft}{
 \urule{$(\conv \vdash)$}
          {$\stc A \vdash Z $}
          {$\conv A \vdash Z$}
}

\newcommand{\convRight}{
 \urule{$(\vdash \conv)$}
          {$Z \vdash \stc A $}
          {$Z \vdash \conv A $}
}

\newcommand{\mimpLeft}{
 \brule{$(\mimp \vdash)$}
          {$X \vdash A $}
          {$B \vdash Y $}
          {$A \mimp B \vdash \ast \stc X \semic Y$}
}

\newcommand{\mimpRight}{
 \urule{$(\vdash \mimp)$}
          {$A \semic X \vdash B $}
          {$X \vdash A \mimp B$}
}

\newcommand{\mifLeft}{
 \brule{$(\mif \vdash)$}
          {$B \vdash Y $}
          {$X \vdash A $}
          {$B \mif A \vdash Y \semic  \ast \stc X$}
}

\newcommand{\mifRight}{
 \urule{$(\vdash \mif)$}
          {$X \semic A \vdash B $}
          {$X \vdash B \mif A$}
}


\newcommand{\compLeft}{
 \urule{$(\circ \vdash)$}
          {$A \semic B \vdash Z $}
          {$A \circ B \vdash Z$}
}

\newcommand{\compRight}{
 \brule{$(\vdash \circ)$}
          {$X \vdash A $}
          {$Y \vdash B$}
          {$X \semic Y \vdash A \circ B $}
}

\newcommand{\morRight}{
 \urule{$(\vdash \mor)$}
          {$Z \vdash A \semic B$}
          {$Z \vdash A \mor B$}
}

\newcommand{\morLeft}{
 \brule{$(\mor \vdash)$}
          {$A \vdash X $}
          {$B \vdash Y$}
          {$A \mor B \vdash X \semic Y $}
}

\newcommand{\bnotLeft}{
 \urule{$(\bnot \vdash)$}
          {$\ast A \vdash Z $}
          {$\bnot A \vdash Z$}
}

\newcommand{\bnotRight}{
 \urule{$(\vdash \bnot)$}
          {$Z \vdash \ast A $}
          {$Z \vdash \bnot A $}
}

\newcommand{\bimpLeft}{
 \brule{$(\bimp \vdash)$}
          {$X \vdash A $}
          {$B \vdash Y $}
          {$A \bimp B \vdash \ast X \comma Y$}
}

\newcommand{\bimpRight}{
 \urule{$(\vdash \bimp)$}
          {$A \comma X \vdash B $}
          {$X \vdash A \bimp B$}
}


\newcommand{\bandLeft}{
 \urule{$(\band \vdash)$}
          {$A \comma  B \vdash Z $}
          {$A \band B \vdash Z$}
}

\newcommand{\bandRight}{
 \brule{$(\vdash \band)$}
          {$X \vdash A$}
          {$Y \vdash B$}
          {$X \comma Y \vdash A \band B $}
}

\newcommand{\borLeft}{
 \brule{$(\bor \vdash)$}
          {$A \vdash X$}
          {$B \vdash Y$}
          {$A \bor B \vdash X \comma Y$}
}

\newcommand{\borRight}{
 \urule{$(\vdash \bor)$}
          {$Z \vdash A \comma B$}
          {$Z \vdash A \bor B $}
}

\newcommand{\BTopLeft}{
 \urule{$(\vdash \btop)$}
          {$I \vdash Z $}
          {$\btop \vdash Z $}
}

\newcommand{\BTopRight}{
\idrule{$(\vdash \btop)$}{$I \vdash \btop$}
}

\newcommand{\BBotRight}{
\urule{$(\vdash \bbot)$}
      {$X \vdash I$}
      {$X \vdash \bbot$}
}

\newcommand{\BBotLeft}{
\idrule{$(\bbot \vdash)$}{$\bbot \vdash I$}
}

\newcommand{\id}{
\idrule{(id)}{$p \vdash p$}
}

\newcommand{\cut}{
\brule{(cut)}
      {$X \vdash A$} 
      {$A \vdash Y$} 
      {$X \vdash Y$} 
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Modal Axioms

\newcommand{\Refl}{
 \urule{(T)}
       {$\blkb X \vdash Y $}
       {$ X \vdash Y$}
}

\newcommand{\Trans}{
 \urule{(4)}
       {$\blkb X \vdash Y $}
       {$\blkb \blkb X \vdash Y$}
}

\newcommand{\Sym}{
 \urule{(B)}
       {$\blkb X \vdash Y $}
       {$ \ast \blkb \ast X \vdash Y$}
}


\begin{document}


\title{ }
\begin{slide}
  \begin{Heading}
A New Machine-checked Proof of Strong Normalisation for Display Logic
  \end{Heading}

\begin{center}
\begin{tabular*}{\linewidth}{@{}l@{\extracolsep{\fill}}l@{}} 
\multicolumn{2}{c}{Jeremy E.\ Dawson and Rajeev Gor\'{e}}
\\ \\
Automated Reasoning Group      & Formal Methods Group                 \\
Computer Sciences Laboratory   & Dept.\ of Computer Science           \\
Res.\ Sch.\ of Inf.\ Sci.\ and Eng.\ & Fac.\ of Eng.\ and Inf.\ Tech. \\
Institute of Advanced Studies  & The Faculties                        \\
\multicolumn{2}{c}{Australian National University}                    \\
\texttt{jeremy@csl.anu.edu.au} \hspace{1cm}  &
                                  \texttt{rpg@csl.anu.edu.au}         \\
\texttt{csl.anu.edu/{\small$\mytilde$}jeremy} &
                        \texttt{csl.anu.edu.au/{\small$\mytilde$}rpg} \\
\end{tabular*}
\end{center}

\begin{itemize}
\small 
\item[ ] Gor{\'e} supported by an Australian Research Council Queen Elizabeth II Fellowship.
   
 \item[ ] Dawson supported by an Australian Research Council Large Research Grant.
\end{itemize}

\end{slide}

\begin{slide}
  \begin{Heading}
    {Overview and Motivation}
  \end{Heading}

  \begin{description}
  \item[RA:] Algebra of binary relations (sets of ordered pairs) 
    over underlying set $U$

    Foundation of relational databases

  \item[Display Calculi:] Generalised sequent framework due to Nuel
    Belnap 

   Single cut-elimination proof if rules
    satisfy 8 easily checked conditions

  \item[dRA:] Display Calculus for the logic of relation algebras 
    
  \item[Isabelle/HOL:] Logical framework that allows us to formalise
    mathematics 

  \item[Goal:] Use Isabelle/HOL to check the strong normalisation proof of
    Wansing

  \item[Actual outcome:] problem with proof, found and checked a new proof

  \end{description}
\end{slide}



\begin{slide}
  \begin{Heading}
    {Display Calculus \Dl{RA} for Relation Algebra}
  \end{Heading}

  \begin{description}
  \item[RA:] 
  Algebra of binary relations (sets of ordered pairs) over underlying set $U$
  Extends classical propositional logic (algebra of sets), we only show
  classical connectives and rules.

  \item[Atomic constants:] $c ::= \bbot \mid 
                                  \btop \mid 
\ldots
%                                  \mtop \mid 
%                                  \mbot $
%                                  \hfill ($\emptyset \mid$
%                                  $U \times U \mid$ identity $\mid$ diversity)
$
    
  \item[Atomic formulae:] $p ::=  p_0  \mid 
                                  p_1  \mid 
                                  p_2  \mid 
                                  \cdots$
                                  \hfill (relation symbols)
    
  \item[Formulae:] 
     $A \ B \hfill ::=     \hfill c          \hfill \mid 
                           \hfill p          \hfill \mid 
                           \hfill \bnot A   \hfill \mid 
                           \hfill A \band B \hfill \mid 
                           \hfill A \bor B  \hfill \mid 
\hfill \ldots 
%                           \hfill \conv A    \hfill \mid 
%                           \hfill A \mand B \hfill \mid 
%                           \hfill A \mor B
$

%  \item \hspace{7cm} $U \times U - A$ \hspace{1.2cm} 
%                     $\cap$ \hspace{2.1cm}
%                     $\cup$ \hspace{1.2cm}
%                     converse 
%                     composition \hspace{0.1cm}



  \item[Structure:] \hfill 
        $X \ Y \hfill ::= \hfill A          \hfill \mid 
                          \hfill I          \hfill \mid
                          \hfill \ast X     \hfill \mid
                          \hfill X \comma Y \hfill \mid 
\hfill \ldots 
%                          \hfill E          \hfill \mid 
%                          \hfill \blob X    \hfill \mid
%                          \hfill X \semic Y \hfill  
$

  \item[Sequent:] \hfill $X \vdash Y$ \hfill where $X$ is the
    \defn{antecedent} and $Y$ is the \defn{succedent}

  \item[Sequent rule:] \hfill 
                        \urule{(name)}
                              {$X_1 \vdash Y_1 \cdots X_n \vdash X_n$}
                              {$X \vdash Y$}
                        \hfill
                        \urule{}
                              {\defn{premisses}}
                              {\defn{conclusion}}

  \end{description}
\end{slide}

\begin{slide}
  \begin{Heading}
    { Display Calculus \Dl{RA}: Display Postulates}
  \end{Heading}

  \begin{description}

  \item[ ]
%    \begin{picture}(500,160)%(30, 0)
    \begin{picture}(500,60)%(30, 0)
    \thicklines
    \put (0,   20) { \AstLeft }         \put (100,   20) { \AstRight }      
    \put (200, 20) { \AstAstLeft }           
    \put (360,  10) { \ResidExt}         \put (500,   10) { \DualResidExt}
%    \put (0,   120) { \AstLeft }         \put (100,   120) { \AstRight }      
%    \put (200, 120) { \AstAstLeft }           
%    \put (380,  120) { \ResidConv }      \put (500, 120) { \ConvConvLeft }
%    \put (0,    10) { \ResidInt}         \put (160,    10) { \DualResidInt}
%    \put (360,  10) { \ResidExt}         \put (500,   10) { \DualResidExt}
    \end{picture}
\vfill
  \item[Theorem (Belnap82):]  For every sequent $X \vdash Y$ and every
    substructure $Z$ of $X \vdash Y$, there is a structurally
    equivalent sequent $Z \vdash Y'$ or $X' \vdash Z$ that has $Z$
    displayed as the whole of its antecedent or succedent.

%  \item[e.g.] \urule{}
%              {$\ast p_3 \vdash p_0 \semic (p_0 \mand p_1) $}
%              {$\ast (p_0 \semic (p_0 \mand p_1)) \vdash p_3$}
%         \urule{}
%              {$\ast p_3 \semic \ast \blob (p_0 \mand p_1) \vdash p_0 $}
%              {$\ast p_3 \vdash p_0 \semic (p_0 \mand p_1) $}
%         \urule{}
%              {$\ast \blob p_0 \semic p_3 \vdash p_0 \mand p_1$}
%              {$\ast p_3 \vdash p_0 \semic (p_0 \mand p_1) $}

  \item[e.g.] \urule{}
              {$\ast p_3 \vdash p_0 \comma (p_0 \band p_1) $}
              {$\ast (p_0 \comma (p_0 \band p_1)) \vdash p_3$}
	 \qquad
         \urule{}
              {$\ast p_3 \comma \ast (p_0 \band p_1) \vdash p_0 $}
              {$\ast p_3 \vdash p_0 \comma (p_0 \band p_1) $}

  \end{description}
\end{slide}

\begin{slide}
  \begin{Heading}
    { Display Calculus \Dl{RA}: Logical Rules} 
  \end{Heading}

  \begin{itemize}
  \item Left and right introduction rules for every logical connective

%  \item 
%    \begin{picture}(300,580)(0,0)
%    \thicklines
%    \put (0,    540) { \mbotLeft}        \put (200,  530) { \mbotRight}
%    \put (0,    490) { \mtopLeft}        \put (200,  500) { \mtopRight}
%    \put (0,    450) { \compLeft}        \put (200,  450) { \compRight}
%    \put (0,    410) { \morLeft}         \put (200,  410) { \morRight}
%%    \put (0,    370) { \mifLeft}         \put (200,  370) { \mifRight}
%%   \put (0,    330) { \mimpLeft}        \put (200,  330) { \mimpRight}
%    \put (0,    290) { \convLeft}        \put (200,  290) { \convRight}
%    \put (0,    250) { \mnotLeft}        \put (200,  250) { \mnotRight}
%    \put (0,    220) { \BBotLeft}        \put (200,  210) { \BBotRight}
%    \put (0,    170) { \BTopLeft}        \put (200,  180) { \BTopRight}
%    \put (0,    130) { \borLeft}         \put (200,  130) { \borRight}
%    \put (0,     90) { \bandLeft}        \put (200,   90) { \bandRight}
%%    \put (0,     50) { \bimpLeft}        \put (200,   50) { \bimpRight}
%    \put (0,     10) { \bnotLeft}        \put (200,   10) { \bnotRight}
%    \end{picture}

\vspace*{-1em}

  \item $\id$ \hfill $\cut$ 
\vspace*{-0.2em}      
  \item $\borLeft$ \hspace{1.5cm} decoding/rewrite \hspace{1.5cm} $\borRight$
\vspace*{-0.2em}
  \item $\bandLeft$ \hspace{3cm} rewrite/decoding \hspace{0.5cm} $\bandRight$
\vspace*{-0.2em}
  \item Introduced formula is always displayed
\vspace*{-0.2em}
  \item Gentzen overloading:
%    \begin{tabular}{ccccccc}
    \begin{tabular}{cccc}
     Antecedent Part & $\btop$ & $\bnot$ & $\band$ \\ % & $\mtop$ & $\mnot$ & $\mand$ \\
     Connective & $I$ & $\ast$ & $\comma$ \\ % & $\myE$ & $\blob$ & $\semic$ \\
     Succedent Part & $\bbot$ & $\bnot$ & $\bor$ % & $\mbot$ &  $\mnot$ & $\mor$
   \end{tabular}
\vspace*{-0.2em}
%     \item Example: $\ast (p_0 \semic p_1) \vdash \ast \blob (p_1 \comma
%       p_3)$ \hfill $\semic$ is $\mor$ and $\comma$ is $\band$
     \item Example: $\ast (p_0 \comma p_1) \vdash \ast (p_1 \comma p_3)$ 
     \quad means \quad $\lnot (p_0 \lor p_1) \vdash \lnot (p_1 \land p_3)$

   \end{itemize}

\end{slide}

\begin{slide}
  \begin{Heading}
    { Display Logic \Dl{RA}: Structural Rules}
  \end{Heading}
  
  A \defn{structural} rule contains no logical connectives and no
  formula variables.
    
%  \begin{picture}(600,250)(30,0)
%  \thicklines
%  
%  \put (0,  210) { \SemicAssLeft}    \put (275,  210) { \CommaAssRight}
%                                     \put (550,  210) { \CommaComRight}
%  \put (0,  100) { \IPlusMinusLeft}  \put (190,  100) { \myEPlusMinusRight}
%                                     \put (400,  100) { \ConvmyERight}
%                                     \put (570,  100) { \ConvTopLeft}
%  \put (0,  0) { \CommaWeakLeft}     \put (300,  0) { \CommaContRight}
%                                     \put (550,  0) { \Tagging}         
%  \end{picture}
  \begin{picture}(600,160)(30,0)
  \thicklines
  
  \put (0,  100) { \IPlusMinusLeft} 
                                     \put (275,  100) { \CommaAssRight}
                                     \put (550,  100) { \CommaComRight}
  \put (0,  0) { \CommaWeakLeft}     \put (300,  0) { \CommaContRight}
  \end{picture}

  \begin{heading}
    { Cut Elimination}
  \end{heading}
  Theorem [Belnap~82]: Any display calculus whose rules obey eight
    conditions given by Belnap enjoys cut-elimination. If $X \vdash Y$
    is derivable, then it is derivable without the cut rule.
    
% \vfill
  % Note: no (M) (P) or (C) rules for $\semic$ since $\mand/\mor$ are
  % not classical connectives

\end{slide}

\comment{
\begin{slide}
  \begin{Heading}
    { Logical Variation Via Structural Rules (modularity)}
  \end{Heading}

  \begin{itemize}
  \item An equation $A \leq B$ is {\bf primitive} iff $A$ and $B$ are
    built from relational variables and the constants $\btop$ and
    $\mtop$ with the help of $\conv$, $\band$, $\bor$ and $\mand$
    only, and if no relational variable appears in $A$ more than once
    (Kracht96).  

  \item[]
    \begin{picture}(600, 80)(20,0)
    \thicklines 
    \put(0,  80) {\mbox{ reflexivity }} 
    \put(160, 80) {\mbox{ seriality}} 
    \put(320, 80) {\mbox{ symmetry}} 
    \put(480, 80) {\mbox{ transitivity}} 
    \put(0,   50) {\mbox{ $(T) \ \mtop \leq A$}}
    \put(140,  50) {\mbox{ $(D) \ A \mand \btop = \btop $}} 
    \put(300, 50) {\mbox{ $(B) \ A = \, \conv\! A$}} 
    \put(460, 50) {\mbox{ $(4) \ A \mand B  \leq A \bor B$}} 
    \put(-10,  0) {\urule{$(T)$}{$X \vdash Z$}
                                {$\myE \vdash Z$}} 
    \put(140,   0) {\invrule{$(D)$}{$I \vdash Z$}
                                  {$X \semic I \vdash Z$}} 
    \put(300,  0) {\invrule{$(B)$}{$\blob X \vdash Z$}
                                  {$X \vdash Z$}} 
    \put(460, 0) {\brule{$(4)$}{$X_{1} \vdash Z$}{$X_{2} \vdash Z$}
                                 {$X_{1} \semic X_{2} \vdash Z$}}
    \end{picture}

  \item Theorem [Belnap~82]: Any display calculus whose rules obey eight
    conditions given by Belnap enjoys cut-elimination. If $X \vdash Y$
    is derivable, then it is derivable without the cut rule.
    
  \item Theorem: Using results of Kracht~96 we can construct a
    \defn{cut-free} display calculus which is sound and complete for
    any primitive extension of RA.

  \end{itemize}
\end{slide}

\begin{slide}
  \begin{Heading}
    {Formalising \Dl{RA} in Logical Frameworks}
  \end{Heading}

  \begin{description}
  \item[Isabelle:] Encode the rules directly using the syntax of Isabelle

  So horizontal line in sequents becomes Isabelle's \ \ \texttt{==>}

  Can construct derivations but no term to represent a derivation

  Cannot reason about derivations

\item[ELF and Isabelle/CTT:] Use dependent type theory

 Have terms to represent derivations

 But reasoning about derivations is still naive

 Written up in an ENTCS paper which appeared in 2001

\item[Conclusion:] require a deep(er) embedding 

  \end{description}

\end{slide}
end of comment}

\begin{slide}
  \begin{Heading}
    {Formalising \Dl{RA} in Isabelle/HOL}
  \end{Heading}

  \begin{itemize}
\item[Formulae:] 
     $A \ B \hfill ::=     \hfill c          \hfill \mid 
                           \hfill p          \hfill \mid 
                           \hfill \bnot A   \hfill \mid 
                           \hfill A \band B \hfill \mid 
                           \hfill A \bor B  \hfill \mid 
\hfill \ldots
%                           \hfill \conv A    \hfill \mid 
%                           \hfill A \mand B \hfill \mid 
%                           \hfill A \mor B
$
  \end{itemize}  

\begin{verbatim}
datatype formula = Btimes formula formula ("_ && _" [68,68] 67)
                 | Bplus formula formula ("_ v _" [64,64] 63)
                 | Bneg formula ("--_" [70] 70)
                 | Btrue ("T")
                 | Bfalse("F")
                 | ...
                 | PP string 
                 | FV string 
\end{verbatim}
%                 | Rtimes formula formula ("_ oo _" [68,68] 67)
%                 | Rplus formula formula ("_ ++ _" [64,64] 63)
%                 | Rneg formula ("_^" [75] 75)
%                 | Rtrue ("r1")
%                 | Rfalse("r0")

\end{slide}


%\begin{slide}
%  \begin{Heading}
%    {Formalising \Dl{RA} in Isabelle/HOL}
%  \end{Heading}

%  \begin{description}
%    \item[Structure:] \hfill 
%        $X \ Y \hfill ::= \hfill A          \hfill \mid 
%                          \hfill I          \hfill \mid
%                          \hfill \ast X     \hfill \mid
%                          \hfill X \comma Y \hfill \mid 
%                          \hfill E          \hfill \mid 
%                          \hfill \blob X    \hfill \mid
%                          \hfill X \semic Y \hfill  $

%     \item[Sequent rule:] \hfill 
%                        \urule{(name)}
%                              {$X_1 \vdash Y_1 \cdots X_n \vdash X_n$}
%                              {$X \vdash Y$}
%                        \hfill
%                        \urule{}
%                              {\defn{premisses}}
%                              {\defn{conclusion}}

%  \end{description}

%\begin{verbatim}
%datatype structr = Comma structr structr 
%                 | SemiC structr structr 
%                 | Star structr  
%                 | Blob structr  
%                 | I | E | Structform formula | SV string   

%datatype sequent = Sequent structr structr       

%datatype rule = Rule (sequent list) sequent 
%              | Bidi sequent sequent
%              | InvBidi sequent sequent 
%\end{verbatim}
  
%\end{slide}


%\begin{slide}
%  \begin{Heading}
%    {Example Rules}
%  \end{Heading}
  
%  Some purely syntactic operators, together with
%  \texttt{print-translation} and \texttt{parse-translation} allow
%  \texttt{Sequent (SV ''X'') ''Y''} to be written as \\
%  \texttt{\$X |- \$Y}

%\vfill

%\invrule{}{$X \vdash Y \semic Z$}{$\ast \blob Y \semic X \vdash Z$}

%\begin{verbatim}
%  defs
%      ss1   "ss1 == Bidi ($''X'' |- $''Y''; $''Z'') 
%                         ( *@$''Y''; $''X'' |- $''Z'')"  
%\end{verbatim}

%\end{slide}


\begin{slide}
  \begin{Heading}
    {Formalising \Dl{RA} in Isabelle/HOL}
  \end{Heading}

  \begin{description}
    \item[Structure:] \hfill 
        $X \ Y \hfill ::= \hfill A          \hfill \mid 
                          \hfill I          \hfill \mid
                          \hfill \ast X     \hfill \mid
                          \hfill X \comma Y \hfill \mid 
\hfill \ldots
%                          \hfill E          \hfill \mid 
%                          \hfill \blob X    \hfill \mid
%                          \hfill X \semic Y \hfill  
$

  \end{description}

\begin{verbatim}
datatype structr = Comma structr structr                '
                 | Star structr                         *
                 | I                                    $I
                 | ...
                 | Structform formula          
                 | SV string                            $''X''
\end{verbatim}
%                 | SemiC structr structr                ;
%                 | Blob structr                         @
%                 | E                                    $E

 \texttt{datatype sequent = Sequent structr structr} \hfill \texttt{|-}
 
 \texttt{\$''X'' |- ''A''} via \texttt{print-translation} and
 \texttt{parse-translation} becomes
 \texttt{Sequent (SV ''X'') (Structform (FV ''A''))}
  
\end{slide}

\begin{slide}
  \begin{Heading}
    {A Deep Embedding of Rules}
  \end{Heading}

  \urule{(name)}{$X_1 \vdash Y_1 \cdots X_n \vdash X_n$}
                      {$X \vdash Y$}
        \hfill
%  \invrule{}{$X \vdash Y \semic Z$}
%            {$\ast \blob Y \semic X \vdash Z$}
  \invrule{}{$X \vdash Y \comma Z$}
            {$\ast Y \comma X \vdash Z$}

  \begin{verbatim}
    datatype rule = Rule (sequent list) sequent 
                  | Bidi sequent sequent
                  | InvBidi sequent sequent 
  \end{verbatim}

%    ss1   "ss1 == Bidi ($''X'' |- $''Y''; $''Z'')
%                       ( *@$''Y''; $''X'' |- $''Z'')"
  \begin{verbatim}
    cs1   "cs1 == Bidi ($''X'' |- $''Y'',, $''Z'') 
                       (*$''Y'',, $''X'' |- $''Z'')"
  \end{verbatim}

Deep embedding of variables -- \texttt{''X''}, not \texttt{?X} --
needed to describe properties of rules (eg Belnap's eight conditions).

This means we must define substitution explicitly.
 
A shallow(er) embedding might not model rules at all.


%\texttt{seqRep b X Y seq1 seq2} holds if 
%\texttt{seq1} and \texttt{seq2} are the same, except that (possibly)
%one or more occurrences of \texttt{X} in \texttt{seq1} appear as
%corresponding occurrences of \texttt{Y} in \texttt{seq2},
%where such differences occur only in succedent (antecedent) positions,
%according as \texttt{b} is \texttt{True} or \texttt{False}. 

\end{slide}

\begin{slide}
  \begin{Heading}
    {Formalising Derivations}
  \end{Heading}
  
\begin{verbatim}
datatype dertree = Der sequent rule (dertree list) 
                 | Unf sequent 
\end{verbatim}

Leaves of successful derivation have form 
\texttt{Der (''A'' |- ''A'') id  []} 

A derived rule will have some \texttt{Unf}inished leaf sequents

\texttt{wfb :: "dertree => bool"} returns true if the end-sequent of
\texttt{dertree} and the end-sequents of its immediate children in
\texttt{dertree list} are a well-formed instance of \texttt{rule} 

\texttt{allDT :: "(dertree => bool) => dertree => bool"} returns true if
every node of \texttt{dertree} satisfies the given boolean valued
function

\texttt{allDT wfb} returns true if every rule application in
\texttt{dertree} is well formed

\texttt{allDT (frb rules)} returns true if every rule application in
\texttt{dertree} is a member of set \texttt{rules}

\end{slide}

\comment{
\begin{slide}
  \begin{Heading}
    {Formalising Derivations}
  \end{Heading}
  
\texttt{IsProvableR :: "rule set => [sequent set, sequent] => bool"}

\begin{verbatim}
idf_der = "IsProvableR rls {} (?p |- ?p)"

 "IsProvableR rules prems concl == (? pftr.
    allDT (frb rules) pftr & allDT wfb pftr &
    conclDT pftr = concl & set (premsDT pftr) <= prems)"

"IsProvable rules (Rule prems concl) = 
        IsProvableR rules (set prems) concl"
\end{verbatim}
  
\end{slide}
end of comment}

\begin{slide}
  \begin{Heading}
    {Reducing a Left-and-Right Principal Cut}
  \end{Heading}
  
  \begin{itemize}
  \item A cut on $A$ is \defn{left- [right-] principal} if the left [right]
    inference immediately above the cut introduces $A$ via a logical
    rule, written $(\vdash A)$ [$(A \vdash)$]


  \item[ ]
         \begin{center}{\small
         \vpf
         \bpf
           \A "$\Pi_{L}$"
           \U "$X \vdash A$" "($\vdash A$)"
           \A "$\Pi_{R}$"
           \U "$A \vdash Y$" "($A \vdash$)"
           \B "$X \vdash Y$"
         \epf
         }\end{center}

  \item C8: All left-and-right principal cuts can be replaced by cuts
    on strictly smaller subformulae of $A$


   \item Base Case:
   \brule{(cut)}
         {$p \vdash p$}
         {$p \vdash p$}
         {$p \vdash p$} reduced to just $p \vdash p$

    \item Similar cases for $\btop$, $\bbot$
%    \item Similar cases for $\btop$, $\mtop$, $\bbot$, $\mbot$
    
      
  \end{itemize}
\end{slide}

\begin{slide}
  \begin{Heading}
    {Example of a Principal reduction (C8 condition)}
  \end{Heading}
  
{\small
\vpf
\bpf
\A "$\Pi_{ZAB}$"
\U "$Z \vdash A, B$"
\U "$Z \vdash A \bor B$" "($\vdash \bor $)"
\A "$\Pi_{AX}$"
\U "$A \vdash X$"
\A "$\Pi_{BY}$"
\U "$B \vdash Y$"
\B [1em] "$A \bor B \vdash X, Y$" "($\bor \vdash $)"
\B [2em] "$Z \vdash X, Y$" "($cut$)"
\U ['] "Principal cut on formula $A \bor B$"
\epf
\hfill
\vpf
\bpf
\A "$\Pi_{ZAB}$"
\U "$Z \vdash A, B$"
\U "$*A, Z \vdash B$" "(dp)"
\A "$\Pi_{BY}$"
\U "$B \vdash Y$"
\B [2em] "$*A, Z \vdash Y$" "($cut$)"
\U "$Z \vdash A, Y$" "(dp)"
\U "$Z, *Y \vdash A$" "(dp)"
\A "$\Pi_{AX}$"
\U "$A \vdash X$"
\B [2em] "$Z, *Y \vdash X$" "($cut$)"
\U "$Z \vdash X, Y$" "(dp)"
\U ['] "Transformed derivation uses cuts only on $A$ and $B$"
\epf
}

\vfill

Must exhibit and hard-wire such transformations for every logical connective

So if cut is \defn{not} left-and-right principal then we try to make
it so ...

\end{slide}

\begin{slide}
  \begin{heading}
    {A Parametric Reduction --- making a cut left-right-principal}
  \end{heading}
  
  \begin{itemize}

  \item Given a derivation ending in a non left-and-right principal
    cut on formula $A$, we trace the ancestor occurrences of this $A$
    up $\Pi_{L}$:

  \item Let $\Pi[A := Y]$ mean ``replace all 
    (non-principal) ancestors of $A$ with $Y$'' 

  \item[]
    \begin{center}
    \vspace{-2ex}
      {\small
      \bpf
      \A "$\Pi^{1}_{L}$"
      \U "$V \vdash A $" "($\vdash A$)"
      \U "$\Pi^{2}_{L}$" "($\pi$)"
      \U "$X \vdash A $" "($\rho$)"
      \A "$\Pi_R$"
      \U "$A \vdash Y$" 
      \B [2em] "$X \vdash Y$" "($cut$)"
      \epf
      \qquad \qquad
      \bpf
      \A "$\Pi^{1}_{L}$"
      \U "$V \vdash A $" "($\vdash A$)"
      \A "$\Pi_R$"
      \U "$A \vdash Y$" 
      \B [2em] "$V \vdash Y$" "($cut$)"
      \U "$\Pi^{2}_L[A := Y]$" "($\pi$)"
      \U "$X \vdash Y $" "($\rho$)"
      \epf
      }
    \end{center}

  \item New cut is left-principal (similarly make it also right principal)

  \item If $\Pi_L$ branches ($A$ introduced at multiple places), more complex
  (!) \\
  If $\Pi^{1}_{L}$ is empty, $A$ introduced
  by $A \vdash A$, no new cuts needed.
  \end{itemize}
\end{slide}


\begin{slide}
  \begin{Heading}
    {Strong Normalisation}
  \end{Heading}
  
Cut-admissibility proceeds by eliminating the top-most cut

Strong normalisation: define reduction steps, eliminate any cut that
can be reduced, and prove that this cut-elimination procedure terminates:
\begin{itemize}
\item $\Pi_n < \Pi_{n-1} < \cdots < \Pi_2 < \Pi_0$
\item $\Pi_n$ is cut-free
\item $n$ is finite
\item weak-normalisation (attacking top most cut) is an instance of this method
\end{itemize}

Usually define reductions as either a parametric or principal move,
with proviso that we must not cross a cut in a parametric move

\end{slide}

\begin{slide}
  \begin{Heading}
    {Why Formalise (in Isabelle) ?}
  \end{Heading}

Strong-normalisation proofs are notoriously difficult involving many cases

We tried to formalise Heinrich Wansing's proof of strong-normalisation
for display logic, but got stuck at one particular case

Found a problem ... Wansing assumes that $\Pi^1_L$ is unchanged! 

      \hfill $V_A$ is $(*A \comma X)$ \hfill 
      $V_Y$ is $(*Y \comma X)$ \hfill \mbox{}


    \begin{center}
      {\small
      \bpf
      \A "$\Pi^{1}_{L}$"
      \U "$V_A \vdash A $" "($\vdash A$)"
      \U "$X \vdash A, A$" "(dp)"
      \U "$X \vdash A $" "(ctr)"
      \A "$\Pi_R$"
      \U "$A \vdash Y$" 
      \B [2em] "$X \vdash Y$" "($cut$)"
      \epf
      \qquad \qquad
      \bpf
      \A "$\Pi'^{1}_{L}$"
      \U "$V_Y \vdash A $" "($\vdash A$)"
      \A "$\Pi_R$"
      \U "$A \vdash Y$" 
      \B [2em] "$V_Y \vdash Y$" "($cut$)"
      \U "$X \vdash Y, Y$" "(dp)"
      \U "$X \vdash Y $" "(ctr)"
      \epf
      }
    \end{center}

% Can construct counter-examples where his proof goes into loops: a
% given cut is reduced to itself ... his procedure will not terminate

\end{slide}

\begin{slide}
\begin{heading}
  { Branch in left subtree --- before and after}
\end{heading}
\begin{center}
\bpf
\A "$\Pi'$"
\U "$X' \vdash A $" "(intro-$A$)"
\A "$\Pi''$"
\U "$X'' \vdash A $" "(intro-$A$)"
\B [1em] "$\Pi_L$" "($\pi$)"
\U "$X \vdash A $" "($\rho$)"
\A "$\Pi_R$"
\U "$A \vdash Y$"
\B [0em] "$X \vdash Y$" "($cut$)"
\epf

\bpf
\A "$\Pi'$"
\U "$X' \vdash A $" % "(intro-$A$)"
\A "$\Pi_R$"
\U "$A \vdash Y$"
\B [1em] "$X' \vdash Y$" "($cut$)"
\A "$\Pi''$"
\U "$X'' \vdash A $" % "(intro-$A$)"
\A "$\Pi_R$"
\U "$A \vdash Y$"
\B [1em] "$X'' \vdash Y$" "($cut$)"
\B [1em] "$\Pi_L[A \,?\!= Y]$" "($\pi$)"
\U "$X \vdash Y $" "($\rho$)"
\epf
\end{center}
\end{slide}

\begin{slide}
\begin{heading}
  { Two successive introductions -- before }
\end{heading}

\begin{center}
\bpf
\A "$\Pi$"
\U "$X, B \vdash * B $" "($\rho$)"
\U "$X, B \vdash \lnot B $" "($\vdash \lnot$)"
\U "$*\lnot B, X \vdash *B $" "(dp)"
\U "$*\lnot B, X \vdash \lnot B $" "($\vdash \lnot$)"
\U "$X \vdash \lnot B, \lnot B $" "(dp)"
\U "$X \vdash \lnot B $" "($\vdash \mbox{cont}$)"
\A "$\Pi_R$"
\U "$\lnot B \vdash Y$"
\B [2em] "$X \vdash Y$" "($cut$)"
\epf
\end{center}
\end{slide}

\begin{slide}
\begin{heading}
  { Two successive introductions -- after }
\end{heading}
\begin{center}
\bpf
\A "$\Pi$"
\U "$X, B \vdash * B $" "($\rho$)"
\U "$X, B \vdash \lnot B $" "($\vdash \lnot$)"
\A "$\Pi_R$"
\U "$\lnot B \vdash Y$"
\B [2em] "$X, B \vdash Y $" "($cut$)"
\U "$*Y, X \vdash * B $" "(dp)"
\U "$*Y, X \vdash \lnot B $" "($\vdash \lnot$)"
\A "$\Pi_R$"
\U "$\lnot B \vdash Y$"
\B [0em] "$*Y, X \vdash Y $" "($cut$)"
\U "$X \vdash Y, Y $" "(dp)"
\U "$X \vdash Y $" "($\vdash \mbox{cont}$)"
\epf
\end{center}
\end{slide}

\begin{slide}
  \begin{Heading}
    {Various Binary Orderings}
  \end{Heading}

\begin{enumerate}
  
\item\label{defn:porders-LRP} $\LRPord{\Pi_1}{\Pi_0}$ if the bottom
  inferences of derivations $\Pi_1$ and $\Pi_0$ are both cut, and
  either
  \begin{enumerate}
  \item\label{defn:porders-LRP-1} the cut in $\Pi_1$ is left-principal
    or right-principal, and the cut in $\Pi_0$ is neither, or
  \item\label{defn:porders-LRP-2} the cut in $\Pi_1$ is (left- and
    right-)principal, and the cut in $\Pi_0$ is not (left- and
    right-)principal.
  \end{enumerate}
  
\item\label{defn:porders-cut} $\cutord{\Pi_1}{\Pi_0}$ if the bottom
  inferences of derivations $\Pi_1$ and $\Pi_0$ are both cut, and if
  either
  \begin{enumerate}
  \item\label{defn:porders-cut-1} the size of the cut-formula of
    $\Pi_1$ is smaller than that of $\Pi_0$, or
  \item\label{defn:porders-cut-2} each derivation has the same
    cut-formula, and $\LRPord{\Pi_1}{\Pi_0}$.
  \end{enumerate}
  
\end{enumerate}

\end{slide}

\begin{slide}
  \begin{Heading}
    {Various Binary Orderings}
  \end{Heading}

\begin{enumerate}

\item\label{defn:porders-sn1} $\snoneord{\Pi_1}{\Pi_0}$ 
  if $\Pi_0$ and $\Pi_1$ are the same except that one of the immediate 
  subtrees of  $\Pi_0$ is strongly normalisable and reduces to the 
  corresponding immediate subtree of $\Pi_1$.
  
\item\label{defn:porders-dt} 
  $\dtord{\Pi_1}{\Pi_0}$ iff any of the following hold:
  \begin{enumerate}

  \item\label{defn:porders-dt-1} the bottom inference of $\Pi_1$ is
    not cut, but that of $\Pi_0$ is
  
  \item\label{defn:porders-dt-2} $\cutord{\Pi_1}{\Pi_0}$
  
  \item $\snoneord{\Pi_1}{\Pi_0}$.
  \end{enumerate}

\end{enumerate}

% \end{slide}

% \begin{slide}
%   \begin{Heading}
%     {Theorems About The Partial Orders}
%   \end{Heading}

\begin{theorem}
  The relations \texttt{LRPorder}, \texttt{cutorder},
  \texttt{sn1order}, and \texttt{dtorder} are well-founded
\end{theorem}
  
  Despite notation, these relations are \textit{not} reflexive, and
  some are \textit{not} transitive.  
  
  Intuitively, $(\Pi_1, \Pi_0) \in \texttt{dtorder}$ means that
  $\Pi_1$ is closer to being cut-free (in some sense) than is $\Pi_0$.

\end{slide}

\begin{slide}
  \begin{Heading}
    {Inheriting Strong Normalisation}
  \end{Heading}

We next define \texttt{snHered}, a property of derivation trees which
indicates that a tree inherits strong normalisation from its immediate
subtrees.

\begin{definition}
  $\Pi$ satisfies \texttt{snHered} iff: if all the immediate subtrees
  of $\Pi$ are strongly normalisable then $\Pi$ is strongly
  normalisable.
\end{definition}

\begin{verbatim}
   snHered_def = "snHered ?dt == 
     set (nextUp ?dt) <= sn_set --> ?dt : sn_set"
\end{verbatim}

\begin{lemma}\label{hereds-sn}
  A derivation tree $\Pi$ is strongly normalisable iff every subtree
  of $\Pi$ has the property \texttt{snHered}.
\end{lemma}

\comment{
Proof: The ``only if'' part uses a clever instantiation of a theorem
generated automatically by Isabelle from the inductive definition of
\texttt{sn\_set}.

The ``if'' part uses induction on the height of $\Pi$ using the
assumption that every subtree of $\Pi$, including itself, has the
property \texttt{snHered}.
}

\end{slide}

\begin{slide}
  \begin{Heading}
    {Key Properties of Reductions}
  \end{Heading}
  
  When we apply a reduction to a cut at the bottom of a tree
  $\Pi_0$, obtaining $\Pi_1$,
  then every subtree $\Pi_1^s$ of $\Pi_1$ which has cut at the bottom
  satisfies one of
  \begin{itemize}
  \item $\Pi_1^s$ is a proper subtree of $\Pi_0$, or 
  \item $\cutord{\Pi_1^s}{\Pi_0}$, because
  \begin{itemize}
  \item (principal reduction) 
   the cut-formula of $\Pi_1^s$ is smaller than that of $\Pi_0$
  \item (parametric reduction) 
   $\Pi_1^s$ and $\Pi_0$ have the same cut-formula and
    $\LRPord{\Pi_1^s}{\Pi_0}$.
  \end{itemize}
  \end{itemize}

\begin{slide}
  \begin{Heading}
    {Strong-Normalisation}
  \end{Heading}
  
  \begin{lemma}\label{dth}
    For a given derivation $\Pi_0$, if all derivation trees
    $\dtord{\Pi'}{\Pi_0}$ have the property \texttt{snHered}, then so
    does $\Pi_0$.
  \end{lemma}

\begin{verbatim}
dth = "ALL dt'. (dt', ?dt) : dtorder --> snHered dt' 
       ==> snHered ?dt" : thm
\end{verbatim}
  
  Proof: The machine-proof is quite complicated, and a careful
  examination of it highlights why the definition of \textit{dtorder}
  needs to be so complex.

\begin{theorem}
    Every derivation tree is strongly normalisable.
\begin{verbatim}
   all_snH = "snHered ?dt"    : thm
   all_sn  = "strongNorm ?dt" : thm
\end{verbatim}
\end{theorem}

Proof: By well-founded induction, it follows from Lemma~\ref{dth} that
every derivation tree satisfies \texttt{snHered}; the result follows
from Lemma~\ref{hereds-sn}. 

\end{slide}

\comment{
  \begin{definition}
    Two derivation trees $\Pi_0$ and $\Pi_1$ satisfy \texttt{nparRedP}
    if every subtree $\Pi_1^s$ of $\Pi_1$ with a bottom inference
    (cut) satisfies either
  \begin{itemize}
  \item[(a)] $\Pi_1^s$ is a proper subtree of $\Pi_0$, or
  \item[(b)] $\Pi_1^s$ and $\Pi_0$ have the same cut-formula and
    $\LRPord{\Pi_1^s}{\Pi_0}$.
  \end{itemize}
  \end{definition}

  \begin{definition}
    Two derivation trees $\Pi_0$ and $\Pi_1$ satisfy \texttt{c8redP}
    if the lowest rule of $\Pi_0$ is cut, and for each subtree
    $\Pi_1^s$ of $\Pi_1$ whose lowest rule is cut, either
  \begin{itemize}
  \item[(a)] $\Pi_1^s$ is a proper subtree of $\Pi_0$, or
  \item[(b)] the cut-formula of $\Pi_1^s$ is smaller than that of the
    lowest rule of $\Pi_0$.
  \end{itemize}
  \end{definition}
  
\begin{theorem}
    Every derivation tree is strongly normalisable,
    using reductions satisfying \texttt{nparRedP} or \texttt{c8redP}.
\end{theorem}
}

\end{slide}

\begin{slide}
  \begin{Heading}
    {Where are we?}
  \end{Heading}

\begin{itemize}
\item We have actually shown using Isabelle that a class of reductions which
we have defined is (small enough to be) strongly normalising.
\item We would like to show that this
class of reductions is correctly defined, ie, it (is large enough that it) 
contains the reductions used by Wansing.
\item We can show that it is large enough to ensure 
cut-elimination.  
This guards against the worst definition errors.
\item We do this by showing that any tree containing a cut admits at least one
reduction in this class.
% this is in file SNCE.ML
Strong normalization then gives cut-elimination.
\end{itemize}

\end{slide}

% \begin{slide}
%   \begin{Heading}
%     {Template}
%   \end{Heading}

% \end{slide}


\begin{slide}
  \begin{Heading}
    {Belnap's Conditions and New C8}
  \end{Heading}

 \begin{center} 
 {\bf Appendix: Belnap's Conditions.}
 \end{center}
 \bigskip
 
 For every sequent rule Belnap82, page~388 first
 defines the following notions: in an application {\em Inf\ } of a
 sequent rule $(\rho)$, ``constituents occurring as part of occurrences
 of structures assigned to structure-variables are defined to be {\bf
   parameters} of {\em Inf\ }; all other constituents are defined as {\bf
   nonparametric}, including those assigned to formula-variables.
 Constituents occupying similar positions in occurrences of structures
 assigned to the same structure-variable are defined as {\bf congruent}
 in {\em Inf}\ ''. 
 %For example, in an instance of the associative rule
 %$(A)$, all constituents of structures assigned to the structure
 %variables are parameters. As usual, the introduction rules for the
 %logical connectives like $(\vdash \mimp)$ involve constituents (side
 %formulae) in the premisses and constituents (principal formulae) in
 %the conclusion that are not parameters.  
 The eight (actually seven)
 conditions shown below are from [Kracht96]:
 \begin{description}%\vspace{-1em}
 \item[{\bf (C1)}] Each formula which is a constituent of some premiss of a
   rule $\rho$ is a subformula of some formula in the conclusion of $\rho$.
 
 \item[{\bf (C2)}] Congruent parameters are occurrences of the same
   structure.
\end{description}

\end{slide}

\begin{slide}

\begin{description}
\vspace*{-2em}
 
 \item[{\bf (C3)}] Each parameter is congruent to at most one constituent in
   the conclusion. Equivalently, no two constituents of the conclusion are
   congruent. % to each other.
 
 \item[{\bf (C4)}] Congruent parameters are either all antecedent parts
   or all succedent parts of their respective sequent.
 
 \item[{\bf (C5)}] If a formula is non-parametric in the conclusion of a
   rule $\rho$, it is either the entire antecedent, or the entire succedent
   % Such a formula is 
   (called a {\bf principal} formula).
 
 \item[{\bf (C6/7)}] Each rule is closed under simultaneous
   substitution of arbitrary structures for congruent parameters.
 
 \item[{\bf (C8)}] If there are inference rules $\rho_{1}$ and $\rho_{2}$ with
   respective conclusions $X \vdash \varphi$ and 
   $\varphi \vdash Y$ with $\varphi$ principal
   in both inferences (in the sense of C5), and if (cut) is applied to yield
   $X \vdash Y$ then, either $X 
   \vdash Y$ is identical to $X \vdash \varphi$ or to
   $\varphi \vdash Y$; 
   or it is possible to pass from the premisses of $\rho_{1}$ and
   $\rho_{2}$ to $X \vdash Y$ by means of inferences 
   falling under (cut) where
   the cut-formula is always a proper subformula of $\varphi$. 
%   If $\varphi$ satisfies
%   the ``if'' part of this condition it is known as a ``matching principal
%   constituent''.
 \end{description}

\end{slide}

\end{document}