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