Display to Labeled Proofs and Back Again for Tense Logics

ACM Transactions on Computational Logic 22 (3):1-31 (2021)
  Copy   BIBTEX

Abstract

We introduce translations between display calculus proofs and labeled calculus proofs in the context of tense logics. First, we show that every derivation in the display calculus for the minimal tense logic Kt extended with general path axioms can be effectively transformed into a derivation in the corresponding labeled calculus. Concerning the converse translation, we show that for Kt extended with path axioms, every derivation in the corresponding labeled calculus can be put into a special form that is translatable to a derivation in the associated display calculus. A key insight in this converse translation is a canonical representation of display sequents as labeled polytrees. Labeled polytrees, which represent equivalence classes of display sequents modulo display postulates, also shed light on related correspondence results for tense logics.

Links

PhilArchive

External links

  • This entry has no external links. Add one.
Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

From Display to Labelled Proofs for Tense Logics.Agata Ciabattoni, Tim Lyon & Revantha Ramanayake - 2018 - In Anil Nerode & Sergei Artemov (eds.), Logical Foundations of Computer Science. Springer International Publishing. pp. 120 - 139.
Bunched Logics Displayed.James Brotherston - 2012 - Studia Logica 100 (6):1223-1254.
Substructural logics on display.R. Goré - 1998 - Logic Journal of the IGPL 6 (3):451-504.
Labeled sequent calculus for justification logics.Meghdad Ghari - 2017 - Annals of Pure and Applied Logic 168 (1):72-111.
Proof analysis in intermediate logics.Roy Dyckhoff & Sara Negri - 2012 - Archive for Mathematical Logic 51 (1-2):71-92.
Proof Theory for Modal Logic.Sara Negri - 2011 - Philosophy Compass 6 (8):523-538.
Predicate logics on display.Heinrich Wansing - 1999 - Studia Logica 62 (1):49-75.

Analytics

Added to PP
2021-10-09

Downloads
172 (#101,984)

6 months
64 (#60,489)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Tim Lyon
Technische Universität Dresden

References found in this work

Modal Logic: Graph. Darst.Patrick Blackburn, Maarten de Rijke & Yde Venema - 2001 - New York: Cambridge University Press. Edited by Maarten de Rijke & Yde Venema.
Modal Logic.Patrick Blackburn, Maarten de Rijke & Yde Venema - 2001 - Studia Logica 76 (1):142-148.
Proof Methods for Modal and Intuitionistic Logics.Melvin Fitting - 1985 - Journal of Symbolic Logic 50 (3):855-856.
Proof Analysis in Modal Logic.Sara Negri - 2005 - Journal of Philosophical Logic 34 (5-6):507-544.
Display logic.Nuel D. Belnap - 1982 - Journal of Philosophical Logic 11 (4):375-417.

View all 26 references / Add more references