Taming Bounded Depth with Nested Sequents

Agata Ciabattoni; Lutz Straßburger; Matteo Tesi

Taming Bounded Depth with Nested Sequents

Agata Ciabattoni
, Lutz Straßburger
, Matteo Tesi

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

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.

Original language	English
Title of host publication	Advances in Modal Logic, AiML 2022
Editors	David Fernandez-Duque, Alessandra Palmigiano, Alessandra Palmigiano, Sophie Pinchinat
Publisher	College Publications
Pages	199-216
Number of pages	18
ISBN (Electronic)	9781848904132
Publication status	Published - 1 Jan 2022
Externally published	Yes
Event	14th Conference on Advances in Modal Logic, AiML 2022 - Rennes, France Duration: 22 Aug 2022 → 25 Aug 2022

Publication series

Name	Advances in Modal Logic
Volume	14

Conference

Conference	14th Conference on Advances in Modal Logic, AiML 2022
Country/Territory	France
City	Rennes
Period	22/08/22 → 25/08/22

Keywords

Bounded Depth Kripke Models
Cut Elimination
Intermediate Logics
Nested Sequents

Cite this

@inproceedings{8985c2e5a83c4edeb0f2a0fb873493d6,

title = "Taming Bounded Depth with Nested Sequents",

abstract = "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{\textquoteright}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.",

keywords = "Bounded Depth Kripke Models, Cut Elimination, Intermediate Logics, Nested Sequents",

author = "Agata Ciabattoni and Lutz Stra{\ss}burger and Matteo Tesi",

year = "2022",

month = jan,

day = "1",

language = "English",

series = "Advances in Modal Logic",

publisher = "College Publications",

pages = "199--216",

editor = "David Fernandez-Duque and Alessandra Palmigiano and Alessandra Palmigiano and Sophie Pinchinat",

booktitle = "Advances in Modal Logic, AiML 2022",

}

Taming Bounded Depth with Nested Sequents. / Ciabattoni, Agata; Straßburger, Lutz; Tesi, Matteo.
Advances in Modal Logic, AiML 2022. ed. / David Fernandez-Duque; Alessandra Palmigiano; Alessandra Palmigiano; Sophie Pinchinat. College Publications, 2022. p. 199-216 (Advances in Modal Logic; Vol. 14).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Taming Bounded Depth with Nested Sequents

AU - Ciabattoni, Agata

AU - Straßburger, Lutz

AU - Tesi, Matteo

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

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 - Pinchinat, Sophie

PB - College Publications

T2 - 14th Conference on Advances in Modal Logic, AiML 2022

Y2 - 22 August 2022 through 25 August 2022

ER -

Taming Bounded Depth with Nested Sequents

Abstract

Publication series

Conference

Keywords

Fingerprint

Cite this