%%
\documentclass{llncs}
% \documentclass[a4paper,11pt]{article}
%\documentclass[twocolumn,a4paper,11pt]{article}

\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{exptrees}
\usepackage{url}
\usepackage{bussproofs}

\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}

\setcounter{secnumdepth}2
\setcounter{tocdepth}2

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

\renewcommand{\qed}{\hfill$\dashv$}

% \newenvironment{proof}{
 % \noindent{\bf Proof:}}{\mbox{\bf Q.E.D.}\vspace{1ex}}

% \newtheorem{definition}{Definition}[section]

% \newtheorem{lemma}{Lemma}[section]

% \newtheorem{corollary}{Corollary}[section]
    
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Preamble

\newcommand\cfile{}

\newcommand\comment[1]{} 
\newcommand\cc[1]{#1} % for label names 

\newcommand\psl{\ensuremath\MQ_{l1} \ldots \MQ_{ln}}
\newcommand\psr{\ensuremath\MQ_{r1} \ldots \MQ_{rm}}

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

\pagestyle{plain}

\begin{document}

% \title{Deep and Shallow Embeddings for Formalising Sequent Calculi
\title{Generic Methods for Formalising Sequent Calculi
       Applied to Provability Logic}


\author{
 Jeremy E.\ Dawson
% \thanks{Supported by an Australian Research Council Large Grant}
 \ \ and \ \
 Rajeev Gor\'e
% \thanks{Contact Author }
% \thanks{Supported by an Australian Research Council QEII Fellowship}
}
\institute{
Logic and Computation Group,
School of Computer Science
\\ The Australian National University,
Canberra ACT 0200, Australia
\\ \url{http://users.rsise.anu.edu.au/~jeremy/} 
\ \ \url{http://users.rsise.anu.edu.au/~rpg/}
}

\date{}
%% Title 
\maketitle

\begin{abstract}
  We describe generic methods for reasoning about multiset-based
  sequent calculi which improve upon the state of the art by allowing
  us to combine shallow and deep embeddings as desired.  Our methods
  are modular, permit explicit structural rules, and are widely
  applicable to many sequent systems, even to other styles of calculi
  like natural deduction and term rewriting systems. We
  describe new axiomatic type classes 
  %for multisets or sequents of  multisets 
  which enable simplification of multiset or sequent expressions using
  existing algebraic manipulation facilities. We demonstrate the
  benefits of our combined approach by formalising in Isabelle/HOL a
  variant of a recent, non-trivial, pen-and-paper proof of
  cut-admissibility for the provability logic {\textbf{GL}}. Our work
  also provides a machine-checked proof to settle the controversy
  surrounding the proof of cut-admissibility for {\textbf{GL}}.
%
\\[1ex]
Keywords: provability logic, machine-checked proof theory, 
interactive theorem proving, proof theory

\end{abstract}

\input{defs}
\input{gls}
\input{bib}
\input{app}

\end{document}

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