%%
%%
\documentclass{llncs}
%\usepackage{makeidx}
%\usepackage{acmnew-xref}

% \usepackage[scrtime]{prelim2e}
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{exptrees}

%\RequirePackage{mathptm}
%\RequirePackage{times}
%\RequirePackage{palatino}

\renewcommand{\today}{\number\day\ 
  \ifcase\month\or
  January\or February\or March\or April\or May\or June\or
  July\or August\or September\or October\or November\or December\fi
  \ \number\year}

%\setlength \parskip {1.0ex}
\setcounter{secnumdepth}2
\setcounter{tocdepth}2

%\newtheorem{theorem}{Theorem}[subsection]

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Preamble

\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{\fiss}{+}

\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\cfile{}
%\renewcommand{\thepage}{\roman{page}}
\newcommand\shrinklist[1]{
\setlength\parskip{#1\parskip}
\setlength\itemsep{#1\itemsep}
\setlength\itemindent{#1\itemindent}
\setlength\topsep{#1\topsep}
}

\newcommand\comment[1]{} 
% \newcommand\cc[1]{} % for label names 
\newcommand\cc[1]{#1} % for label names 
% \renewcommand\footnote[1]{} % for footnotes
% \pagestyle{myheadings}

\newcommand\url[1]{\texttt{#1}} % in Raj's bibliography

\newcommand\invrule[2]{ 
% for use in non-math mode, args interpreted in math mode
  \begin{tabular}{@{}c@{}}
  $ #1 $ \\ \hline \hline $ #2 $
  \end{tabular}}
\newcommand\slrule[2]{ % similar to \frac, except
% for use in non-math mode, args interpreted in math mode
  \begin{tabular}{@{}c@{}}
  $ #1 $ \\ \hline $ #2 $
  \end{tabular}}

\renewcommand\theenumi{(\alph{enumi})}
\renewcommand\labelenumi{\theenumi}
\renewcommand\theenumii{(\roman{enumii})}
\renewcommand\labelenumii{\theenumii}

%\newcommand\proof{\noindent\textbf{Proof.}}
\newcommand\src[1]{source file \texttt{#1}}
\newcommand\apsrc[1]{Appendix \ref{app:code}}
%\newcommand\seesrc[1]{(see source file \texttt{#1}, \apsrc{#1})}
\newcommand\seesrc[1]{(see source file \texttt{#1})}
%\newcommand\insrc[1]{in source file \texttt{#1} (see \apsrc{#1})}
\newcommand\insrc[1]{in source file \texttt{#1}}
\newcommand\page[1]{page~\pageref{#1}}
\newcommand\fig[1]{Fig.~\ref{fig:#1}}
\newcommand\ch[1]{Chapter~\ref{ch:#1}}
\newcommand\tbl[1]{Table~\ref{tbl:#1}}
\newcommand\thrm[1]{Theorem~\ref{thrm:#1}}
\newcommand\lem[1]{Lemma~\ref{lem:#1}}
\newcommand\ttl[1]{\tti{#1}\label{#1}}
\newcommand\ttdl[1]{\texttt{#1}\tti{#1}\label{#1}}
\newcommand\ttdef[1]{\texttt{#1}\tti{#1}}
\newcommand\tti[1]{\index{#1@\texttt{#1}}}
\newcommand\bfi[1]{\textbf{#1}\index{#1|textbf}}
\newcommand\dRA{{\boldmath $\delta$}\textbf{RA}}
\newcommand\dKt{{\boldmath $\delta$}\textbf{Kt}}
\newcommand\NRA{\textbf{NRA}}
\newcommand\RA{\textbf{RA}}
%\newcommand\M{$\mathcal M$}
\newcommand\M{\ensuremath{\mathcal M}}
\newcommand\Mp{$\mathcal M'$}
\newcommand\up[1]{\vspace{-#1ex}} 
\newcommand\vpf{\vspace{-3ex}} % to reduce space before proof tree
\newcommand\1{\textbf 1}
\newcommand\0{\textbf 0}
\newcommand\cut{(\emph{cut})}
\newcommand\pt{\texttt{pt}}
\newcommand\ptn{\texttt{ptn}}

\newcommand{\blob}{\bullet}

% automatically defined in LLNCS style
%\newtheorem{thm}{Theorem}%[chapter]
%\newtheorem{lemma}[thm]{Lemma}
%\newtheorem{defn}[thm]{Definition}
%\newtheorem{cor}{Corollary}[thm]
%\renewcommand\thecor{\thethm(\arabic{cor})}

\pagestyle{plain}

\begin{document}

\title{Machine-checked Proofs of Cut-elimination and Strong
       Normalisation for Display Logic} 
\author{Jeremy E. Dawson
\thanks{Supported by an Australian Research Council Large Grant}
\and Rajeev Gor\'e 
\thanks{Supported by an Australian Research Council QEII Fellowship}}
\institute{Department of Computer Science and
Automated Reasoning Project, \\ 
Australian National University,
Canberra ACT 0200, Australia \\ 
\texttt{jeremy@arp.anu.edu.au}, \ \ 
\texttt{rpg@arp.anu.edu.au}
%\\[1ex]
%Tel: +61-2-6249-5138 \ \ Fax: +61-2-6249-0010
}

\date{\today}

%% Title 
\maketitle

\begin{abstract}
  We describe a deep embedding of the display calculus for relation
  algebras \dRA\ in the logical framework Isabelle/HOL. We give a
  machine-checked proof of admissibility of cut for\dRA\ using this
  embedding. Our formalisation generalises easily to handle other
  display calculi. We then consider a published proof of strong
  normalisation of cut-elimination for Display Logic, and discuss the
  problems with it which prevented us from being able to formalise it.
  We give a different proof and describe its formalisation in
  Isabelle/HOL.
  \\[1ex]
  Keywords: display logic, cut elimination, strong normalisation,
  machine-checked proof theory, non-classical logics, automated
  deduction, proof systems for relation algebra
\end{abstract}

\tableofcontents

\sloppy 

% \newpage

%% Here begins the main text

\newcommand\file{}

\renewcommand\file{intro.tex}
\markboth{\mbox{}\hfill\today\hfill\file}{\today\hfill\file\hfill}
\input{intro}
\renewcommand\file{pt.tex}
\markboth{\mbox{}\hfill\today\hfill\file}{\today\hfill\file\hfill}
\input{pt}
\renewcommand\file{meth.tex}
\markboth{\mbox{}\hfill\today\hfill\file}{\today\hfill\file\hfill}
\input{meth}
\renewcommand\file{rep.tex}
\markboth{\mbox{}\hfill\today\hfill\file}{\today\hfill\file\hfill}
\input{rep}
\renewcommand\file{mlp.tex}
\markboth{\mbox{}\hfill\today\hfill\file}{\today\hfill\file\hfill}
\input{mlp}
\renewcommand\file{princ.tex}
\markboth{\mbox{}\hfill\today\hfill\file}{\today\hfill\file\hfill}
\input{princ}
\renewcommand\file{putt.tex}
\markboth{\mbox{}\hfill\today\hfill\file}{\today\hfill\file\hfill}
\input{putt}
\renewcommand\file{props.tex}
\markboth{\mbox{}\hfill\today\hfill\file}{\today\hfill\file\hfill}
\input{props}
\renewcommand\file{wans.tex}
\markboth{\mbox{}\hfill\today\hfill\file}{\today\hfill\file\hfill}
\input{wans}
\renewcommand\file{sn.tex}
\markboth{\mbox{}\hfill\today\hfill\file}{\today\hfill\file\hfill}
\input{sn}

\renewcommand\file{confw.tex}
\markboth{\mbox{}\hfill\today\hfill\file}{\today\hfill\file\hfill}
\input{confw}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Here begins the end matter

%\newpage
%\input{bib}

\bibliography{./ce,/home/discus/disk1/rpg/bib/fm,/home/discus/disk1/rpg/bib/modal,/home/discus/disk1/rpg/bib/mtl,/home/discus/disk1/rpg/bib/logic,/home/discus/disk1/rpg/bib/tl,/home/discus/disk1/rpg/bib/paracon,/home/discus/disk1/rpg/bib/linear,/home/discus/disk1/rpg/bib/algebra,/home/discus/disk1/rpg/bib/relevant,/home/discus/disk1/rpg/bib/dl}

\bibliographystyle{plain}

\end{document}