LBI Cut Elimination Proof with BI-MultiCut

Ryuta Arisaka, Shengchao Qin

    Research output: Chapter in Book/Report/Conference proceedingConference contribution


    Cut elimination in sequent calculus is indispensable in bounding the number of distinct formulas to appear during a backward proof search. A usual approach to prove cut admissibility is permutation of derivation trees. Extra care must be taken, however, when contraction appears as an explicit inference rule. In G1i for example, a simple-minded permutation strategy comes short around contraction interacting directly with cut formulas, which entails irreducibility of the derivation height of Cut instances. One of the practices employed to overcome this issue is the use of MultiCut (the “mix” rule) which takes into account the eject of contraction within. A more recent substructural logic BI inherits the characteristics of the intuitionistic logic but also those of multiplicative linear logic (without exponentials). Following Pym's original work, the cut admissibility in LBI (the original BI sequent calculus) is supposed to hold with the same tweak. However, there is a critical issue in the approach: MultiCut does not take care of the eject of structural contraction that LBI permits. In this paper, we show a proper proof of the LBI cut admissibility based on another derivable rule BI-MultiCut.
    Original languageEnglish
    Title of host publication2012 Sixth International Symposium on Theoretical Aspects of Software Engineering
    ISBN (Print) 9781467323536
    Publication statusPublished - 2012
    Event6th International Symposium on Theoretical Aspects of Software Engineering - Beijing, China
    Duration: 4 Jul 20126 Jul 2012
    Conference number: 6


    Conference6th International Symposium on Theoretical Aspects of Software Engineering
    Abbreviated titleTASE 2012


    Dive into the research topics of 'LBI Cut Elimination Proof with BI-MultiCut'. Together they form a unique fingerprint.

    Cite this