On nested sequents for constructive modal logics

Ryuta Arisaka; Anupam Das; Lutz Strassburger

doi:10.2168/LMCS-11(3:7)2015

On nested sequents for constructive modal logics

Ryuta Arisaka
, Anupam Das
, Lutz Strassburger

NRIA, 1 rue Honoré d’Estienne d’Orves

Résultats de recherche: Contribution à un journal › Article › Revue par des pairs

18 Citations (Scopus)

Résumé

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.

langue originale	Anglais
Numéro d'article	7
journal	Logical Methods in Computer Science
Volume	11
Numéro de publication	3
Les DOIs	https://doi.org/10.2168/LMCS-11(3:7)2015
état	Publié - 3 sept. 2015
Modification externe	Oui

Accès au document

10.2168/LMCS-11(3:7)2015

Contient cette citation

@article{ba7b5cda402f49678e2252ed04e79319,

title = "On nested sequents for constructive modal logics",

abstract = "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.",

keywords = "Cut-elimination, Intuitionistic logic, Modal logic, Nested sequents",

author = "Ryuta Arisaka and Anupam Das and Lutz Strassburger",

note = "Publisher Copyright: {\textcopyright} R. Arisaka, Anupam Das, and Lutz Stra{\ss}burger.",

year = "2015",

month = sep,

day = "3",

doi = "10.2168/LMCS-11(3:7)2015",

language = "English",

volume = "11",

journal = "Logical Methods in Computer Science",

issn = "1860-5974",

publisher = "Logical Methods in Computer Science",

number = "3",

}

TY - JOUR

T1 - On nested sequents for constructive modal logics

AU - Arisaka, Ryuta

AU - Das, Anupam

AU - Strassburger, Lutz

N1 - Publisher Copyright: © R. Arisaka, Anupam Das, and Lutz Straßburger.

PY - 2015/9/3

Y1 - 2015/9/3

N2 - 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.

AB - 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.

KW - Cut-elimination

KW - Intuitionistic logic

KW - Modal logic

KW - Nested sequents

U2 - 10.2168/LMCS-11(3:7)2015

DO - 10.2168/LMCS-11(3:7)2015

M3 - Article

AN - SCOPUS:84943635019

SN - 1860-5974

VL - 11

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

IS - 3

M1 - 7

ER -

On nested sequents for constructive modal logics

Résumé

Accès au document

Empreinte digitale

Contient cette citation