HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Proof Translations 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 order to study proof translations in BI logic, we consider first the bunched sequent calculus LBI and then define a new labelled sequent calculus, called GBI. We propose a procedure that translates LBI proofs into GBI proofs and prove its soundness. Moreover we discuss some steps towards the reverse translation of GBI proofs into LBI proofs and propose an algorithm that is illustrated by some examples. Further work will be devoted to its correctness and also to the design of translations of LBI proofs to TBI (labelled-tableaux) proofs.
Document type :
Conference papers
Complete list of metadata

Contributor : Didier Galmiche Connect in order to contact the contributor
Submitted on : Wednesday, October 28, 2020 - 5:05:54 PM
Last modification on : Monday, February 7, 2022 - 10:04:06 AM


  • HAL Id : hal-02982654, version 1



Didier Galmiche, Michel Marti, Daniel Méry. Proof Translations in BI Logic. International Workshop on External and Internal Calculi for Non-Classical Logics, EICNCL 2018, 2018, Oxford, United Kingdom. ⟨hal-02982654⟩



Record views