%%
\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{Mechanisation of Proofs of Interpolation for Display Logic} % Jeremy
% \title{Mechanising Craig Interpolation for Substructural Logics} % James
\title{Machine-checked Interpolation Theorems for Substructural Logics using
Display Calculi} % Raj



\author{
 Jeremy E.\ Dawson\inst{1}%
\thanks{Supported by Australian Research Council Discovery Grant DP120101244}
\and
 James Brotherston\inst{2}%
\thanks{Supported by an EPSRC Career Acceleration Fellowship}
\and
 Rajeev Gor\'e\inst{1}
% \thanks{Contact Author }
% \thanks{Supported by an Australian Research Council QEII Fellowship}
}
\institute{
%Logic and Computation Group,
Research School of Computer Science,
Australian National University
%Canberra ACT 0200, Australia
\and
Queen Mary College, University of London, UK
%\\
% \url{http://users.cecs.anu.edu.au/~jeremy/}
% \ \ \url{http://users.cecs.anu.edu.au/~rpg/}
% \ \ \url{http://www.eecs.qmul.ac.uk/~jamesb/}
} 

\date{}
%% Title 
\maketitle

\begin{abstract}
We give mechanised proofs of Craig interpolation for 
a class of propositional substructural logics using display calculi.

We discuss the difficulties caused by various rules, such as the
binary logical introduction rules in their additive and multiplicative forms,
and the weakening and unit weakening rules.

We also describe the differences between our proofs and those of
Brotherston and Gor\'e, differences motivated by the ease of formalising
the definitions used in intermediate lemmas,
and we detail how we proved the more difficult cases,
such as the weakening rules and the multiplicative binary logical
introduction rules.

Finally, we discuss the value for this work of
using a prover with a programmable user interface
(in our case, Isabelle with its Standard ML interface).
%
\\[1ex]
Keywords:
Craig interpolation,
display logic,
interactive theorem proving,
proof theory

\end{abstract}

\input{defs}
\input{interp}
\input{bib}
\input{app}

\end{document}

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