Annals of Pure and Applied Logic 58 (3):229-246 (1992)
| 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.
|
| Keywords | No keywords specified (fix it) |
| Categories | (categorize this paper) |
| DOI | 10.1016/0168-0072(92)90029-y |
| Options |
Mark as duplicate
Export citation
Request removal from index
|
Download options
References found in this work BETA
Constructive Modal Logics I.Duminda Wijesekera - 1990 - Annals of Pure and Applied Logic 50 (3):271-301.
Citations of this work BETA
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.
An Approach to Infinitary Temporal Proof Theory.Stefano Baratella & Andrea Masini - 2004 - Archive for Mathematical Logic 43 (8):965-990.
Modal Sequent Calculi Labelled with Truth Values: Completeness, Duality and Analyticity.Paulo Mateus, Amílcar Sernadas, Cristina Sernadas & Luca Viganò - 2004 - Logic Journal of the IGPL 12 (3):227-274.
Temporal Gödel-Gentzen and Girard Translations.Norihiro Kamide - 2013 - Mathematical Logic Quarterly 59 (1-2):66-83.
View all 7 citations / Add more citations
Similar books and articles
Cut-Elimination and Proof-Search for Bi-Intuitionistic Logic Using Nested Sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 2008 - In Carlos Areces & Robert Goldblatt (eds.), Advances in Modal Logic, Volume 7. 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.
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.
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 index
2014-01-16
Total views
28 ( #370,728 of 2,409,938 )
Recent downloads (6 months)
8 ( #87,245 of 2,409,938 )
2014-01-16
Total views
28 ( #370,728 of 2,409,938 )
Recent downloads (6 months)
8 ( #87,245 of 2,409,938 )
How can I increase my downloads?
Downloads
