%
\documentclass[orivec]{llncs}


\usepackage[margin=1in]{geometry}

%\usepackage{microtype}%if unwanted, comment out or use option "draft"

\usepackage{proof}
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{url}
\usepackage{cmll}
\usepackage{MnSymbol}
\usepackage{graphicx}
\usepackage{bussproofs}
\usepackage[all]{xy}
\usepackage{comment}
\usepackage{lscape}
\usepackage{ntheorem}

% Theorem evironments

%\renewtheorem{remark}{Remark}
\renewtheorem{theorem}{Theorem}
\renewtheorem{lemma}[theorem]{Lemma}
\renewtheorem{corollary}[theorem]{Corollary}
\renewtheorem{proposition}[theorem]{Proposition}
\renewtheorem{definition}[theorem]{Definition} 

%\newcommand{\excl}{\mathrel{\rotatebox[origin=c]{180}{\ensuremath \multimap}}}

%\usepackage{txfonts}
%\usepackage{amsthm}

\renewcommand{\labelenumi}{(\roman{enumi})}

\def\punit{\bot}
\def\tunit{\mathrm{I}}
%\def\sunit{\Phi}
\def\sunit{\cdot}
\def\limp{\multimap}
\def\excl{\leftY}
%\def\excl{{-\!\!\!<}}
\def\ltens{\otimes}
\def\merge{\bullet}

\def\seq{\Rightarrow}
%\def\seq{>}

\def\fill{\mathrm{FILL}}
\def\biill{\mathrm{BiILL}}
\def\biilldc{\mathrm{BiILL}{\scriptstyle dc}}
%\def\fbills{\mathrm{BiILL}^{sn}}
\def\biillsn{\mathrm{BiILL}{\scriptstyle sn}}
%\def\fbilld{\mathrm{BiILL}^{dn}}
\def\biilldn{\mathrm{BiILL}{\scriptstyle dn}}
\def\filldc{\mathrm{FILL}{\scriptstyle dc}}
%\def\filld{\mathrm{FILL}^{dn}}
\def\filldn{\mathrm{FILL}{\scriptstyle dn}}
\def\impl{\supset}
\def\dimpl{\subset}
\def\bang{!}
\def\qm{?}

\def\drp{\mathit{drp}}
\def\rp{\mathit{rp}}

\newcommand{\binop}{\heartsuit}

\newcommand \seqtodisp[1]{\ulcorner{#1}\urcorner}
\newcommand\disptoseq[1]{\llcorner{#1}\lrcorner}
\def\Pc{\mathcal{P}}
\def\Qc{\mathcal{Q}}
\def\Sc{\mathcal{S}}
\def\Tc{\mathcal{T}}
\def\Uc{\mathcal{U}}
\def\Vc{\mathcal{V}}
\def\Xc{\mathcal{X}}
\def\Yc{\mathcal{Y}}
\def\Zc{\mathcal{Z}}

\def\turn{\vdash}
%\newcommand{\comment}[1]{}

%%%%
%%%% Raj's defs. Need to be merged but want to chat with Ranald first
%%%%

%\def\fill{FILL}
\def\ill{ILL}
\def\mill{MILL}
\def\bill{BILL}
%\def\biill{BiILL}
\def\jill{JILL}
\def\gill{GILL}
\def\dill{DILL}

\def\gnab{?}
\def\adcn{\wedge}
\def\addn{\vee}
\def\adim{\to}
\def\adtp{\top}
\def\adbt{\bot}
\def\mldn{\parr}
\def\mlcn{\otimes}
\def\mltp{\mathbf{1}}
\def\mlbt{\bot}
\def\mlim{\multimap}
\def\mlli{\multimap^{-1}}
\def\mlri{\multimap}
\def\mlrx{
       \mbox{\,\raisebox{0.14ex}{$\scriptstyle>$}\!\!\raisebox{0.14ex}{$\scriptstyle -$}\,}}
\def\mllx{\excl}
%\def\mllx{
%       \mbox{\,\raisebox{0.13ex}{$\scriptstyle-$}\!\!\raisebox{0.13ex}{$\scriptstyle <$}\,}}

\def\sequent{\vdash}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\title{Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic
-- Extended Version}
\author{Ranald Clouston \and Jeremy Dawson \and Rajeev Gor\'e 
\and Alwen Tiu
}
\institute{Logic and Computation Group, Research School of Computer Science,\\
The Australian National University, Canberra ACT 0200, Australia}


\begin{document}

\maketitle

\begin{abstract}
Full Intuitionistic Linear Logic (FILL) is multiplicative
intuitionistic linear logic extended with par. Its proof theory has
been notoriously difficult to get right, and existing sequent calculi
all involve inference rules with complex annotations to guarantee
soundness and cut-elimination. We give a simple and annotation-free
display calculus for FILL which satisfies Belnap's generic
cut-elimination theorem. To do so, our display calculus actually
handles an extension of FILL, called Bi-Intuitionistic Linear Logic
(BiILL), with an `exclusion' connective defined via an adjunction with
par. We refine our display calculus for BiILL into a cut-free nested
sequent calculus with deep inference in which the explicit structural
rules of the display calculus become admissible. A separation property
guarantees that proofs of FILL formulae in the deep inference calculus
contain no trace of exclusion.  Each such rule is sound for the
semantics of FILL, thus our deep inference calculus and display
calculus are conservative over FILL. The deep inference calculus also
enjoys the subformula property and terminating backward proof search,
which gives the NP-completeness of BiILL and FILL.
\end{abstract}
% \begin{abstract}
% Full Intuitionistic Linear Logic (FILL) is multiplicative
% intuitionistic linear logic extended with par. Its proof theory has
% been notoriously difficult to get right, and existing sequent calculi
% all involve inference rules with complex annotations to guarantee
% soundness and cut-elimination. We give a simple annotation-free
% display calculus for FILL which satisfies Belnap's generic
% cut-elimination theorem. To do so, it is necessary to move to an
% extension of FILL, called Bi-Intuitionistic Linear Logic (BiILL), with
% an `exclusion' connective defined via an adjunction with par. We show
% that our display calculus is conservative over FILL via a novel
% sequent rewriting procedure. Since the structural rules of display
% calculi are bad for proof search, we show how they can be absorbed by
% refining our calculus to a cut-free nested sequent calculus with deep
% inference. Our resulting deep-inference calculus enjoys a separation
% property, which allows us to obtain complete fragments of BiILL,
% including FILL. It also enjoys the subformula property, which enables
% terminating backward proof-search and allows us to prove the
% NP-completeness of BiILL and FILL.
% \end{abstract}


\input{intro}

\input{display}
%\input{biill_to_fill}

\input{shallow}
\input{deep}
\input{equiv}
\input{conserv}

\input{concl}

%\vspace*{-1em}
\bibliographystyle{abbrv}
\bibliography{biblio}

\newpage
\appendix
\input{apx}

%\newpage
%\input{junk}
\end{document}


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "root"
%%% End: 
