Proof Translations in BI Logic - Université de Lorraine Accéder directement au contenu
Communication Dans Un Congrès Année : 2018

Proof Translations in BI Logic

Didier Galmiche
Daniel Méry

Résumé

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

Dates et versions

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

Identifiants

  • HAL Id : hal-02982654 , version 1

Citer

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

Partager

Gmail Facebook X LinkedIn More