TY - GEN
T1 - Taming Bounded Depth with Nested Sequents
AU - Ciabattoni, Agata
AU - Straßburger, Lutz
AU - Tesi, Matteo
N1 - Publisher Copyright:
© 2022 College Publications. All rights reserved.
PY - 2022/1/1
Y1 - 2022/1/1
N2 - Bounded depth refers to a property of Kripke frames that serve as semantics for intuitionistic logic. We introduce nested sequent calculi for the intermediate logics of bounded depth. Our calculi are obtained in a modular way by adding suitable structural rules to a variant of Fitting’s calculus for intuitionistic propositional logic, for which we present the first syntactic cut elimination proof. This proof modularly extends to the new nested sequent calculi introduced in this paper.
AB - Bounded depth refers to a property of Kripke frames that serve as semantics for intuitionistic logic. We introduce nested sequent calculi for the intermediate logics of bounded depth. Our calculi are obtained in a modular way by adding suitable structural rules to a variant of Fitting’s calculus for intuitionistic propositional logic, for which we present the first syntactic cut elimination proof. This proof modularly extends to the new nested sequent calculi introduced in this paper.
KW - Bounded Depth Kripke Models
KW - Cut Elimination
KW - Intermediate Logics
KW - Nested Sequents
UR - https://www.scopus.com/pages/publications/85164697813
M3 - Conference contribution
AN - SCOPUS:85164697813
T3 - Advances in Modal Logic
SP - 199
EP - 216
BT - Advances in Modal Logic, AiML 2022
A2 - Fernandez-Duque, David
A2 - Palmigiano, Alessandra
A2 - Palmigiano, Alessandra
A2 - Pinchinat, Sophie
PB - College Publications
T2 - 14th Conference on Advances in Modal Logic, AiML 2022
Y2 - 22 August 2022 through 25 August 2022
ER -