Cut-elimination for the mu-calculus with one variable
We establish syntactic cut-elimination for the one-variable fragment of the modal mu-calculus. Our method is based on a recent cut-elimination technique by Mints that makes use of Buchholz' Omega-rule.
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2012-02-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1202.3501v1 |
| _version_ | 1811253957509513216 |
|---|---|
| author | Grigori Mints Thomas Studer |
| author_facet | Grigori Mints Thomas Studer |
| author_sort | Grigori Mints |
| collection | DOAJ |
| description | We establish syntactic cut-elimination for the one-variable fragment of the modal mu-calculus. Our method is based on a recent cut-elimination technique by Mints that makes use of Buchholz' Omega-rule. |
| first_indexed | 2024-04-12T16:58:49Z |
| format | Article |
| id | doaj.art-cdd19500ef3b48a99888e9978d65655e |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-12T16:58:49Z |
| publishDate | 2012-02-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-cdd19500ef3b48a99888e9978d65655e2022-12-22T03:24:07ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802012-02-0177Proc. FICS 2012475410.4204/EPTCS.77.7Cut-elimination for the mu-calculus with one variableGrigori MintsThomas StuderWe establish syntactic cut-elimination for the one-variable fragment of the modal mu-calculus. Our method is based on a recent cut-elimination technique by Mints that makes use of Buchholz' Omega-rule.http://arxiv.org/pdf/1202.3501v1 |
| spellingShingle | Grigori Mints Thomas Studer Cut-elimination for the mu-calculus with one variable Electronic Proceedings in Theoretical Computer Science |
| title | Cut-elimination for the mu-calculus with one variable |
| title_full | Cut-elimination for the mu-calculus with one variable |
| title_fullStr | Cut-elimination for the mu-calculus with one variable |
| title_full_unstemmed | Cut-elimination for the mu-calculus with one variable |
| title_short | Cut-elimination for the mu-calculus with one variable |
| title_sort | cut elimination for the mu calculus with one variable |
| url | http://arxiv.org/pdf/1202.3501v1 |
| work_keys_str_mv | AT grigorimints cuteliminationforthemucalculuswithonevariable AT thomasstuder cuteliminationforthemucalculuswithonevariable |