Conference Papers Year : 2018

Proof Translations in BI Logic

Didier Galmiche
Daniel Méry

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.
No file

Dates and versions

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

Identifiers

  • HAL Id : hal-02982654 , version 1

Cite

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⟩
71 View
0 Download

Share

More