From Display to Labelled Proofs for Tense Logics

A. Ciabattoni, T. Lyon*, R. Ramanayake

*Bijbehorende auteur voor dit werk

OnderzoeksoutputAcademicpeer review

6 Citaten (Scopus)

Samenvatting

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 .
Originele taal-2English
TitelLogical Foundations of Computer Science
RedacteurenSergei Artemov, Anil Nerode
UitgeverijSpringer
Pagina's120-139
Aantal pagina's20
ISBN van elektronische versie978-3-319-72056-2
ISBN van geprinte versie978-3-319-72055-5
DOI's
StatusPublished - 2018
Extern gepubliceerdJa
EvenementInternational Symposium, LFCS 2018 - Deerfield Beach, United States
Duur: 8-jan-201811-jan-2018

Publicatie series

NaamLecture Notes in Computer Science (LNCS)
UitgeverijSpringer
Volume10703

Conference

ConferenceInternational Symposium, LFCS 2018
Land/RegioUnited States
StadDeerfield Beach
Periode08/01/201811/01/2018

Citeer dit