From Bunches to Labels and Back in BI Logic - Université de Lorraine Access content directly
Conference Papers Year :

From Bunches to Labels and Back in BI Logic

Didier Galmiche
Daniel Méry


In this work we study proof translations in BI logic. In this context we first define a labelled sequent calculus, called GBI, in which labels and constraints reflect the Kripke monoidal resource semantics (KRM) of BI, with total (and not partial) composition of resources and explicit inconsistent resources. After proving the soundness of GBI w.r.t. KRM structures, we show how to translate any LBI-proof (proof of the LBI sequent calculus) into GBI-proof. We also consider the problem of translating GBI-proofs back into LBI-proofs. Noticing that every LBI-translated GBI-proof enjoys a tree-like property on the structure of labels, We show that any GBI-proof that preserves this tree-like property can systematically be translated into an LBI-proof.
No file

Dates and versions

hal-02986801 , version 1 (03-11-2020)


  • HAL Id : hal-02986801 , version 1


Didier Galmiche, Michel Marti, Daniel Méry. From Bunches to Labels and Back in BI Logic. Int. Workshop Syntax meets Semantics, SYSMICS 2019, 2019, Amsterdam, Netherlands. ⟨hal-02986801⟩
52 View
0 Download


Gmail Facebook Twitter LinkedIn More