Bunched Hypersequent Calculi for Distributive Substructural Logics

Agata Ciabattoni, Revantha Ramanayake

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


We introduce a new proof-theoretic framework which enhances the expressive power of bunched sequents by extending them with a hypersequent structure. A general cut-elimination theorem that applies to bunched hypersequent calculi satisfying general rule conditions is then proved. We adapt the methods of transforming axioms into rules to provide cutfree bunched hypersequent calculi for a large class of logics extending the distributive commutative Full Lambek calculus DFLe and Bunched Implication logic BI. The methodology is then used to formulate new logics equipped with a cutfree calculus in the vicinity of Boolean BI.
Original languageEnglish
Title of host publicationLPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
EditorsThomas Eiter, David Sands
Number of pages18
Publication statusPublished - 2017
Externally publishedYes

Publication series

NameEPiC Series in Computing

Cite this