From Display to Labelled Proofs for Tense Logics

In Anil Nerode & Sergei Artemov (eds.), Logical Foundations of Computer Science. Springer International Publishing. pp. 120 - 139 (2018)
Download Edit this record How to cite View on PhilPapers
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.
Categories
(categorize this paper)
PhilPapers/Archive ID
LYOFDT-2
Upload history
Archival date: 2019-09-20
View other versions
Added to PP index
2019-09-20

Total views
129 ( #30,872 of 52,923 )

Recent downloads (6 months)
61 ( #9,346 of 52,923 )

How can I increase my downloads?

Downloads since first upload
This graph includes both downloads from PhilArchive and clicks on external links on PhilPapers.