From Display to Labelled Proofs for Tense Logics

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

Beitragende

Abstract

We introduce an effective translation from proofs in the display calculus to proofs in the labelled calculus in the context of tense logics. We identify the labelled calculus proofs in the image of this translation as those built from labelled sequents whose underlying directed graph possesses certain properties. For the basic normal tense logic Kt, the image is shown to be the set of all proofs in the labelled calculus G3Kt.

Details

OriginalspracheEnglisch
TitelLogical Foundations of Computer Science
Redakteure/-innenSergei Artemov, Anil Nerode
ErscheinungsortCham
Herausgeber (Verlag)Springer International Publishing AG
Seiten120-139
Seitenumfang20
ISBN (Print)978-3-319-72056-2
PublikationsstatusVeröffentlicht - 2018
Peer-Review-StatusJa

Externe IDs

Scopus 85039457502
ORCID /0000-0003-3214-0828/work/142249480