Skip to Main content Skip to Navigation
Conference papers

Relating Labelled and Label-Free Bunched Calculi in BI Logic

Didier Galmiche 1 Michel Marti 1 Daniel Méry 1 
1 TYPES - Logic, Proof Theory and Programming
LORIA - FM - Department of Formal Methods
Abstract : In this paper we study proof translations between labelled and label-free calculi for the logic of Bunched Implications (BI). We first consider the bunched sequent calculus LBI and define a labelled sequent calculus, called GBI, in which labels and constraints reflect the properties of a specifically tailored Kripke resource semantics of BI with two total resource composition operators and explicit internalization of inconsistency. After showing the soundness of GBI w.r.t. our specific Kripke frames, we show how to translate any LBI-proof into a GBI-proof. Building on the properties of that translation we devise a tree property that every LBI-translated GBI-proof enjoys. We finally show that any GBI-proof enjoying this tree property (and not only LBI-translated ones) can systematically be translated to an LBI-proof.
Document type :
Conference papers
Complete list of metadata
Contributor : Didier GALMICHE Connect in order to contact the contributor
Submitted on : Wednesday, October 28, 2020 - 4:07:40 PM
Last modification on : Monday, February 7, 2022 - 10:04:06 AM


  • HAL Id : hal-02982509, version 1



Didier Galmiche, Michel Marti, Daniel Méry. Relating Labelled and Label-Free Bunched Calculi in BI Logic. 28th International Conference on Automated Reasoning with Anamytic Tableaux and Related Methods, TABLEAUX 2019, 2019, Londres, United Kingdom. pp.130-146. ⟨hal-02982509⟩



Record views