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: 91,386

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

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.
An approach to infinitary temporal proof theory.Stefano Baratella & Andrea Masini - 2004 - Archive for Mathematical Logic 43 (8):965-990.
Bunched Logics Displayed.James Brotherston - 2012 - Studia Logica 100 (6):1223-1254.
A note on the proof theory the λII-calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
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.
Proof-Theoretic Semantics, Self-Contradiction, and the Format of Deductive Reasoning.Peter Schroeder-Heister - 2012 - Topoi 31 (1):77-85.
Classical non-associative Lambek calculus.Philippe de Groote & François Lamarche - 2002 - Studia Logica 71 (3):355-388.
Classical Non-Associative Lambek Calculus.Philippe De Groote & François Lamarche - 2002 - Studia Logica 71 (3):355 - 388.
The deduction rule and linear and near-linear proof simulations.Maria Luisa Bonet & Samuel R. Buss - 1993 - Journal of Symbolic Logic 58 (2):688-709.
A proof-search procedure for intuitionistic propositional logic.R. Alonderis - 2013 - Archive for Mathematical Logic 52 (7-8):759-778.
The cost of a cycle is a square.A. Carbone - 2002 - Journal of Symbolic Logic 67 (1):35-60.
Sequent calculus proof theory of intuitionistic apartness and order relations.Sara Negri - 1999 - Archive for Mathematical Logic 38 (8):521-547.
Minimum propositional proof length is NP-Hard to linearly approximate.Michael Alekhnovich, Sam Buss, Shlomo Moran & Toniann Pitassi - 2001 - Journal of Symbolic Logic 66 (1):171-191.

Analytics

Added to PP
2014-01-16

Downloads
39 (#399,999)

6 months
7 (#418,426)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Proof Theory for Functional Modal Logic.Shawn Standefer - 2018 - Studia Logica 106 (1):49-84.
Distributed First Order Logic.Chiara Ghidini & Luciano Serafini - 2017 - Artificial Intelligence 253 (C):1-39.
A proof-theoretic investigation of a logic of positions.Stefano Baratella & Andrea Masini - 2003 - Annals of Pure and Applied Logic 123 (1-3):135-162.

View all 15 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