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

\input{app_labels} % for references to Appendix if Appendix not included


\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 allow % 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}},
  % next two lines added 10/6
  where we abstract a large part of the proof in a way which is
  immediately applicable to 
%other logics.
  other calculi.
  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, cut admissibility,
interactive theorem proving, proof theory

\end{abstract}

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

% following line needs to be present to get references to Appendix
% if not, uncomment \input{app_labels} at the beginning
% \input{app} % not for proceedings version

\end{document}

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