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

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

\pagestyle{plain}

\begin{document}

\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 general methods for reasoning about multiset-based
  sequent calculi and show how they allow us to mix-and-match shallow
  and deep embeddings. Our methods are modular, permit explicit
  structural rules, and are widely applicable to other sequent
  systems, even to other derivation systems. We also describe new
  axiomatic type classes relevant to multisets and sequents of
  multisets. We demonstrate the benefits of our approach by
  formalising a variant of a recent, non-trivial, pen-and-paper proof
  of cut-admissibility for the provability logic {\textbf{GL}} in
  Isabelle/HOL. Our work confirms that the controversy surrounding the
  proof of cut-admissibility for {\textbf{GL}} has finally been settled.
\end{abstract}

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

\end{document}

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