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)
  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

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

Comparing modal sequent systems.Greg Restall - unknown
Proof analysis in intermediate logics.Roy Dyckhoff & Sara Negri - 2012 - Archive for Mathematical Logic 51 (1):71-92.
Propositional quantifiers in labelled natural deduction for normal modal logic.Matteo Pascucci - 2019 - Logic Journal of the IGPL 27 (6):865-894.
Bunched Logics Displayed.James Brotherston - 2012 - Studia Logica 100 (6):1223-1254.
A tableau calculus with automaton-labelled formulae for regular grammar logics.Rajeev Gore - unknown
Substructural logics on display.R. Goré - 1998 - Logic Journal of the IGPL 6 (3):451-504.
A Labelled Deductive System for Relational Semantics of the Lambek Calculus.Miroslawa Kolowska-Gawiejnowicz - 1999 - Mathematical Logic Quarterly 45 (1):51-58.
Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic. CSLI Publications. pp. 43-66.
Proof Theory for Modal Logic.Sara Negri - 2011 - Philosophy Compass 6 (8):523-538.
Hypothetical Logic of Proofs.Eduardo Bonelli & Gabriela Steren - 2014 - Logica Universalis 8 (1):103-140.
An Analytic Calculus for the Intuitionistic Logic of Proofs.Brian Hill & Francesca Poggiolesi - 2019 - Notre Dame Journal of Formal Logic 60 (3):353-393.
Reasoning About Collectively Accepted Group Beliefs.Raul Hakli & Sara Negri - 2011 - Journal of Philosophical Logic 40 (4):531-555.
On semilattice relevant logics.Ryo Kashima - 2003 - Mathematical Logic Quarterly 49 (4):401.
Labelled non-classical logics.Luca Viganò - 2000 - Boston: Kluwer Academic Publishers.
On proof terms and embeddings of classical substructural logics.Ken-Etsu Fujita - 1998 - Studia Logica 61 (2):199-221.

Analytics

Added to PP
2019-09-20

Downloads
435 (#42,603)

6 months
61 (#68,473)

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.
Cut-free sequent calculi for some tense logics.Ryo Kashima - 1994 - Studia Logica 53 (1):119 - 135.
Geometrisation of first-order logic.Roy Dyckhoff & Sara Negri - 2015 - Bulletin of Symbolic Logic 21 (2):123-163.
Power and weakness of the modal display calculus.Marcus Kracht - 1996 - In H. Wansing (ed.), Proof Theory of Modal Logic. Kluwer Academic Publishers. pp. 93--121.

View all 6 references / Add more references