On Nested Sequents for Constructive Modal Logics
We present deductive systems for various modal logics that can be obtained from the constructive variant of the normal modal logic CK by adding combinations of the axioms d, t, b, 4, and 5. This includes the constructive variants of the standard modal logics K4, S4, and S5. We use for our presentati...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2015-09-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1583/pdf |
| _version_ | 1811225317637881856 |
|---|---|
| author | Lutz Strassburger Anupam Das Ryuta Arisaka |
| author_facet | Lutz Strassburger Anupam Das Ryuta Arisaka |
| author_sort | Lutz Strassburger |
| collection | DOAJ |
| description | We present deductive systems for various modal logics that can be obtained
from the constructive variant of the normal modal logic CK by adding
combinations of the axioms d, t, b, 4, and 5. This includes the constructive
variants of the standard modal logics K4, S4, and S5. We use for our
presentation the formalism of nested sequents and give a syntactic proof of cut
elimination. |
| first_indexed | 2024-04-12T09:05:03Z |
| format | Article |
| id | doaj.art-7f423a55d1af4dd7bebb8d7ddd2e270e |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-12T09:05:03Z |
| publishDate | 2015-09-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-7f423a55d1af4dd7bebb8d7ddd2e270e2022-12-22T03:39:07ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742015-09-01Volume 11, Issue 310.2168/LMCS-11(3:7)20151583On Nested Sequents for Constructive Modal LogicsLutz StrassburgerAnupam DasRyuta ArisakaWe present deductive systems for various modal logics that can be obtained from the constructive variant of the normal modal logic CK by adding combinations of the axioms d, t, b, 4, and 5. This includes the constructive variants of the standard modal logics K4, S4, and S5. We use for our presentation the formalism of nested sequents and give a syntactic proof of cut elimination.https://lmcs.episciences.org/1583/pdfcomputer science - logic in computer science |
| spellingShingle | Lutz Strassburger Anupam Das Ryuta Arisaka On Nested Sequents for Constructive Modal Logics Logical Methods in Computer Science computer science - logic in computer science |
| title | On Nested Sequents for Constructive Modal Logics |
| title_full | On Nested Sequents for Constructive Modal Logics |
| title_fullStr | On Nested Sequents for Constructive Modal Logics |
| title_full_unstemmed | On Nested Sequents for Constructive Modal Logics |
| title_short | On Nested Sequents for Constructive Modal Logics |
| title_sort | on nested sequents for constructive modal logics |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/1583/pdf |
| work_keys_str_mv | AT lutzstrassburger onnestedsequentsforconstructivemodallogics AT anupamdas onnestedsequentsforconstructivemodallogics AT ryutaarisaka onnestedsequentsforconstructivemodallogics |