Effective Cut-elimination for a Fragment of Modal mu-calculus

Studia Logica 100 (1-2):279-287 (2012)
  Copy   BIBTEX

Abstract

A non-effective cut-elimination proof for modal mu-calculus has been given by G. Jäger, M. Kretz and T. Studer. Later an effective proof has been given for a subsystem M 1 with non-iterated fixpoints and positive endsequents. Using a new device we give an effective cut-elimination proof for M 1 without restriction to positive sequents

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,438

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

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.
A Simple Proof that Super-Consistency Implies Cut Elimination.Gilles Dowek & Olivier Hermant - 2012 - Notre Dame Journal of Formal Logic 53 (4):439-456.
A note on the proof theory the λII-calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
Indexed systems of sequents and cut-elimination.Grigori Mints - 1997 - Journal of Philosophical Logic 26 (6):671-696.
Proof normalization modulo.Gilles Dowek & Benjamin Werner - 2003 - Journal of Symbolic Logic 68 (4):1289-1316.
Cut-elimination for simple type theory with an axiom of choice.G. Mints - 1999 - Journal of Symbolic Logic 64 (2):479-485.
Bunched Logics Displayed.James Brotherston - 2012 - Studia Logica 100 (6):1223-1254.
The Computational Content of Arithmetical Proofs.Stefan Hetzl - 2012 - Notre Dame Journal of Formal Logic 53 (3):289-296.

Analytics

Added to PP
2012-02-08

Downloads
29 (#542,067)

6 months
8 (#347,703)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

An extension of the omega-rule.Ryota Akiyoshi & Grigori Mints - 2016 - Archive for Mathematical Logic 55 (3-4):593-603.

Add more citations

References found in this work

Syntactic cut-elimination for common knowledge.Kai Brünnler & Thomas Studer - 2009 - Annals of Pure and Applied Logic 160 (1):82-95.

Add more references