Relating Labelled and Label-Free Bunched Calculi in BI Logic - Université de Lorraine
Communication Dans Un Congrès Année : 2019

Relating Labelled and Label-Free Bunched Calculi in BI Logic

Didier Galmiche
Daniel Méry

Résumé

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.
Fichier non déposé

Dates et versions

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

Identifiants

  • HAL Id : hal-02982509 , version 1

Citer

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⟩
97 Consultations
0 Téléchargements

Partager

More