Relating Labelled and Label-Free Bunched Calculi in BI Logic - Université de Lorraine Access content directly
Conference Papers Year : 2019

Relating Labelled and Label-Free Bunched Calculi in BI Logic

Didier Galmiche
Daniel Méry


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

Dates and versions

hal-02982509 , version 1 (28-10-2020)


  • 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⟩
88 View
0 Download


Gmail Mastodon Facebook X LinkedIn More