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 metadatas
Contributor : Didier Galmiche <>
Submitted on : Wednesday, October 28, 2020 - 5:05:54 PM
Last modification on : Friday, November 13, 2020 - 3:45:56 PM


  • 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