Skip to Main content Skip to Navigation
Conference papers

From Bunches to Labels and Back 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 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.
Document type :
Conference papers
Complete list of metadatas

https://hal.univ-lorraine.fr/hal-02986801
Contributor : Didier Galmiche <>
Submitted on : Tuesday, November 3, 2020 - 11:52:53 AM
Last modification on : Thursday, November 5, 2020 - 3:33:04 AM

Identifiers

  • HAL Id : hal-02986801, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

8