Journal of Philosophical Logic 26 (6):671-696 (1997)
Abstract |
Cut reductions are defined for a Kripke-style formulation of modal logic in terms of indexed systems of sequents. A detailed proof of the normalization (cutelimination) theorem is given. The proof is uniform for the propositional modal systems with all combinations of reflexivity, symmetry and transitivity for the accessibility relation. Some new transformations of derivations (compared to standard sequent formulations) are needed, and some additional properties are to be checked. The display formulations [1] of the systems considered can be presented as encodings of Kripke-style formulations
|
Keywords | Philosophy |
Categories | (categorize this paper) |
Reprint years | 2004 |
DOI | 10.1023/A:1017948105274 |
Options |
![]() ![]() ![]() ![]() |
Download options
References found in this work BETA
Semantical Analysis of Intuitionistic Logic I.Saul A. Kripke - 1963 - In Michael Dummett & J. N. Crossley (eds.), Formal Systems and Recursive Functions: Proceedings of the Eighth Logic Colloquium, Oxford July 1963. North Holland. pp. 92-130.
Proof Methods for Modal and Intuitionistic Logics.Melvin Fitting - 1985 - Journal of Symbolic Logic 50 (3):855-856.
View all 6 references / Add more references
Citations of this work BETA
Display to Labeled Proofs and Back Again for Tense Logics.Agata Ciabattoni, Tim Lyon, Revantha Ramanayake & Alwen Tiu - 2021 - ACM Transactions on Computational Logic 22 (3):1-31.
Shifting Priorities: Simple Representations for Twenty-Seven Iterated Theory Change Operators.Hans Rott - 2006 - In David Makinson, Jacek Malinowski & Heinrich Wansing (eds.), Towards Mathematical Philosophy. Dordrecht: Springer. pp. 269–296.
Proofnets for S5: Sequents and Circuits for Modal Logic.Greg Restall - 2007 - In C. Dimitracopoulos, L. Newelski & D. Normann (eds.), Logic Colloquium 2005. Cambridge: Cambridge University Press. pp. 151-172.
View all 19 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.
Valentini’s Cut-Elimination for Provability Logic Resolved.Rajeev Goré & Revantha Ramanayake - 2012 - Review of Symbolic Logic 5 (2):212-238.
A Cut-Free Gentzen Formulation of Basic Propositional Calculus.Kentaro Kikuchi & Katsumi Sasaki - 2003 - Journal of Logic, Language and Information 12 (2):213-225.
Protoalgebraic Gentzen Systems and the Cut Rule.Àngel J. Gil & Jordi Rebagliato - 2000 - Studia Logica 65 (1):53-89.
On Some Proof Theoretical Properties of the Modal Logic GL.Marco Borga - 1983 - Studia Logica 42 (4):453 - 459.
Proof Normalization Modulo.Gilles Dowek & Benjamin Werner - 2003 - Journal of Symbolic Logic 68 (4):1289-1316.
Analytics
Added to PP index
2009-01-28
Total views
40 ( #283,723 of 2,507,555 )
Recent downloads (6 months)
1 ( #416,983 of 2,507,555 )
2009-01-28
Total views
40 ( #283,723 of 2,507,555 )
Recent downloads (6 months)
1 ( #416,983 of 2,507,555 )
How can I increase my downloads?
Downloads