Annotation-free sequent calculi for full intuitionistic linear logic

Ranald Clouston*, Jeremy Dawson, Rajeev Goré, Alwen Tiu

*Corresponding author for this work

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    12 Citations (Scopus)

    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 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.

    Original languageEnglish
    Title of host publicationLeibniz International Proceedings in Informatics, LIPIcs
    EditorsSimona Ronchi Della Rocca
    PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
    Pages197-214
    Number of pages18
    ISBN (Electronic)9783939897606
    DOIs
    Publication statusPublished - 1 Sept 2013
    Event22nd Annual Conference of the European Association for Computer Science Logic EACSL, CSL 2013 - Torino, Italy
    Duration: 2 Sept 20135 Sept 2013

    Publication series

    NameLeibniz International Proceedings in Informatics, LIPIcs
    Volume23
    ISSN (Print)1868-8969

    Conference

    Conference22nd Annual Conference of the European Association for Computer Science Logic EACSL, CSL 2013
    Country/TerritoryItaly
    CityTorino
    Period2/09/135/09/13

    Fingerprint

    Dive into the research topics of 'Annotation-free sequent calculi for full intuitionistic linear logic'. Together they form a unique fingerprint.

    Cite this