TY - GEN
T1 - Annotation-free sequent calculi for full intuitionistic linear logic
AU - Clouston, Ranald
AU - Dawson, Jeremy
AU - Goré, Rajeev
AU - Tiu, Alwen
N1 - Publisher Copyright:
© Ranald Clouston, Jeremy Dawson, Rajeev Goré, and Alwen Tiu.
PY - 2013/9/1
Y1 - 2013/9/1
N2 - 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 cutelimination 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.
AB - 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 cutelimination 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.
KW - Deep inference
KW - Display calculus
KW - Linear logic
KW - Nested sequent calculus
UR - http://www.scopus.com/inward/record.url?scp=84906755472&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.CSL.2013.197
DO - 10.4230/LIPIcs.CSL.2013.197
M3 - Conference contribution
T3 - Leibniz International Proceedings in Informatics, LIPIcs
SP - 197
EP - 214
BT - Leibniz International Proceedings in Informatics, LIPIcs
A2 - Della Rocca, Simona Ronchi
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 22nd Annual Conference of the European Association for Computer Science Logic EACSL, CSL 2013
Y2 - 2 September 2013 through 5 September 2013
ER -