From Bunches to Labels and Back in BI Logic
Résumé
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.