2-Sequent calculus: a proof theory of modalities

Annals of Pure and Applied Logic 58 (3):229-246 (1992)
  Copy   BIBTEX

Abstract

Masini, A., 2-Sequent calculus: a proof theory of modalities, Annals of Pure and Applied Logic 58 229–246. In this work we propose an extension of the Getzen sequent calculus in order to deal with modalities. We extend the notion of a sequent obtaining what we call a 2-sequent. For the obtained calculus we prove a cut elimination theorem.

Categories

Keywords

Reprint years

DOI

10.1016/0168-0072(92)90029-y

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 94,045

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

Proof nets sequentialisation in multiplicative linear logic.Paolo Di Giamberardino & Claudia Faggian - 2008 - Annals of Pure and Applied Logic 155 (3):173-182.
A proof-theoretic treatment of λ-reduction with cut-elimination: λ-calculus as a logic programming language.Michael Gabbay - 2011 - Journal of Symbolic Logic 76 (2):673 - 699.
Canonical proof nets for classical logic.Richard McKinley - 2013 - Annals of Pure and Applied Logic 164 (6):702-732.
Sufficient conditions for cut elimination with complexity analysis.João Rasga - 2007 - Annals of Pure and Applied Logic 149 (1-3):81-99.
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.
A proof-search procedure for intuitionistic propositional logic.R. Alonderis - 2013 - Archive for Mathematical Logic 52 (7-8):759-778.
Cut-elimination and a permutation-free sequent calculus for intuitionistic logic.Roy Dyckhoff & Luis Pinto - 1998 - Studia Logica 60 (1):107-118.
Intuitionistic sequent calculi for finitely many-valued logics.E. Reznik & P. Curmin - 2001 - Logic Journal of the IGPL 9 (6):793-812.
An approach to infinitary temporal proof theory.Stefano Baratella & Andrea Masini - 2004 - Archive for Mathematical Logic 43 (8):965-990.
Linear logic with fixed resources.Dmitry A. Archangelsky & Mikhail A. Taitslin - 1994 - Annals of Pure and Applied Logic 67 (1-3):3-28.

Analytics

Added to PP
2014-01-16

Downloads
41 (#378,911)

6 months
7 (#592,005)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Natural deduction calculi for classical and intuitionistic S5.S. Guerrini, A. Masini & M. Zorzi - 2023 - Journal of Applied Non-Classical Logics 33 (2):165-205.
Proof Theory for Functional Modal Logic.Shawn Standefer - 2018 - Studia Logica 106 (1):49-84.
Cut Elimination for Extended Sequent Calculi.Simone Martini, Andrea Masini & Margherita Zorzi - 2023 - Bulletin of the Section of Logic 52 (4):459-495.
Distributed First Order Logic.Chiara Ghidini & Luciano Serafini - 2017 - Artificial Intelligence 253 (C):1-39.

View all 16 citations / Add more citations

References found in this work

Proofs and types.Jean-Yves Girard - 1989 - New York: Cambridge University Press.
Intuitionistic tense and modal logic.W. B. Ewald - 1986 - Journal of Symbolic Logic 51 (1):166-179.
Constructive modal logics I.Duminda Wijesekera - 1990 - Annals of Pure and Applied Logic 50 (3):271-301.

Add more references