From Display to Labelled Proofs for Tense Logics

, &
In Sergei Artemov & Anil Nerode (eds.), Logical Foundations of Computer Science (Lecture Notes in Computer Science 7734). Springer. pp. 120 - 139 (2013)
  Copy   BIBTEX

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

Keywords

Reprint years

Other Versions

No versions found

Links

PhilArchive

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Display to Labeled Proofs and Back Again for Tense Logics.Agata Ciabattoni, Tim Lyon, Revantha Ramanayake & Alwen Tiu - 2021 - ACM Transactions on Computational Logic 22 (3):1-31.
On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems.Tim Lyon - 2013 - In Sergei Artemov & Anil Nerode (eds.), Logical Foundations of Computer Science (Lecture Notes in Computer Science 7734). Springer. pp. 177-194.
Propositional quantifiers in labelled natural deduction for normal modal logic.Matteo Pascucci - 2019 - Logic Journal of the IGPL 27 (6):865-894.
Comparing modal sequent systems.Greg Restall - unknown
Refining Labelled Systems for Modal and Constructive Logics with Applications.Tim Lyon - 2021 - Dissertation, Technischen Universität Wien
Herzberger’s Limit Rule with Labelled Sequent Calculus.Andreas Fjellstad - 2020 - Studia Logica 108 (4):815-855.
A Labelled Deductive System for Relational Semantics of the Lambek Calculus.Miroslawa Kolowska-Gawiejnowicz - 1999 - Mathematical Logic Quarterly 45 (1):51-58.
Nested Sequents for Intuitionistic Modal Logics via Structural Refinement.Tim Lyon - 2021 - In Anupam Das & Sara Negri (eds.), Automated Reasoning with Analytic Tableaux and Related Methods: TABLEAUX 2021. pp. 409-427.
Proof Systems for Two-Way Modal Mu-Calculus.Bahareh Afshari, Sebastian Enqvist, Graham E. Leigh, Johannes Marti & Yde Venema - forthcoming - Journal of Symbolic Logic:1-50.
A tableau calculus with automaton-labelled formulae for regular grammar logics.Rajeev Gore - unknown

Analytics

Added to PP
2019-09-20

Downloads
542 (#41,034)

6 months
121 (#52,458)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Tim Lyon
Technische Universität Dresden

Citations of this work

Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics.Tim Lyon & Kees van Berkel - 2019 - In M. Baldoni, M. Dastani, B. Liao, Y. Sakurai & R. Zalila Wenkstern (eds.), PRIMA 2019: Principles and Practice of Multi-Agent Systems. Springer. pp. 202-218.

Add more citations

References found in this work

Proof Analysis in Modal Logic.Sara Negri - 2005 - Journal of Philosophical Logic 34 (5-6):507-544.
Proof analysis in intermediate logics.Roy Dyckhoff & Sara Negri - 2012 - Archive for Mathematical Logic 51 (1):71-92.
Geometrisation of First-Order Logic.Roy Dyckhoff & Sara Negri - 2015 - Bulletin of Symbolic Logic 21 (2):123-163.
Cut-free sequent calculi for some tense logics.Ryo Kashima - 1994 - Studia Logica 53 (1):119 - 135.
Power and weakness of the modal display calculus.Marcus Kracht - 1996 - In Heinrich Wansing (ed.), Proof theory of modal logic. Boston: Kluwer Academic Publishers. pp. 93--121.

View all 6 references / Add more references