Sequentialising Nested Systems

Elaine Pimentel; Revantha Ramanayake; Björn Lellmann

doi:10.1007/978-3-030-29026-9_9

Sequentialising Nested Systems

Elaine Pimentel^*, Revantha Ramanayake, Björn Lellmann

^*Corresponding author for this work

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

3 Citations (Scopus)

Abstract

In this work, we investigate the proof theoretic connections between sequent and nested proof calculi. Specifically, we identify general conditions under which a nested calculus can be transformed into a sequent calculus by restructuring the nested sequent derivation (proof) and shedding extraneous information to obtain a derivation of the same formula in the sequent calculus. These results are formulated generally so that they apply to calculi for intuitionistic, normal modal logics and negative modalities.

Original language	English
Title of host publication	Automated Reasoning with Analytic Tableaux and Related Methods
Editors	Serenella Cerrito, Andrei Popescu
Publisher	Springer
Pages	147-165
Number of pages	19
ISBN (Electronic)	978-3-030-29026-9
ISBN (Print)	978-3-030-29025-2
DOIs	https://doi.org/10.1007/978-3-030-29026-9_9
Publication status	Published - 2019
Externally published	Yes
Event	28th International Conference, TABLEAUX 2019 - London, United Kingdom Duration: 3-Sep-2019 → 5-Sep-2019

Conference

Conference	28th International Conference, TABLEAUX 2019
Country/Territory	United Kingdom
City	London
Period	03/09/2019 → 05/09/2019

Access to Document

10.1007/978-3-030-29026-9_9

Embargoed Document

Sequentialising Nested Systems
Final publisher's version, 772 KB
Request copy

Cite this

@inproceedings{e15fb3b014e8463f92c98a1ca7212a68,

title = "Sequentialising Nested Systems",

abstract = "In this work, we investigate the proof theoretic connections between sequent and nested proof calculi. Specifically, we identify general conditions under which a nested calculus can be transformed into a sequent calculus by restructuring the nested sequent derivation (proof) and shedding extraneous information to obtain a derivation of the same formula in the sequent calculus. These results are formulated generally so that they apply to calculi for intuitionistic, normal modal logics and negative modalities.",

author = "Elaine Pimentel and Revantha Ramanayake and Bj{\"o}rn Lellmann",

year = "2019",

doi = "10.1007/978-3-030-29026-9_9",

language = "English",

isbn = "978-3-030-29025-2",

pages = "147--165",

editor = "Cerrito, {Serenella } and Popescu, {Andrei }",

booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods",

publisher = "Springer",

note = "28th International Conference, TABLEAUX 2019 ; Conference date: 03-09-2019 Through 05-09-2019",

}

TY - GEN

T1 - Sequentialising Nested Systems

AU - Pimentel, Elaine

AU - Ramanayake, Revantha

AU - Lellmann, Björn

PY - 2019

Y1 - 2019

N2 - In this work, we investigate the proof theoretic connections between sequent and nested proof calculi. Specifically, we identify general conditions under which a nested calculus can be transformed into a sequent calculus by restructuring the nested sequent derivation (proof) and shedding extraneous information to obtain a derivation of the same formula in the sequent calculus. These results are formulated generally so that they apply to calculi for intuitionistic, normal modal logics and negative modalities.

AB - In this work, we investigate the proof theoretic connections between sequent and nested proof calculi. Specifically, we identify general conditions under which a nested calculus can be transformed into a sequent calculus by restructuring the nested sequent derivation (proof) and shedding extraneous information to obtain a derivation of the same formula in the sequent calculus. These results are formulated generally so that they apply to calculi for intuitionistic, normal modal logics and negative modalities.

U2 - 10.1007/978-3-030-29026-9_9

DO - 10.1007/978-3-030-29026-9_9

M3 - Conference contribution

SN - 978-3-030-29025-2

SP - 147

EP - 165

BT - Automated Reasoning with Analytic Tableaux and Related Methods

A2 - Cerrito, Serenella

A2 - Popescu, Andrei

PB - Springer

T2 - 28th International Conference, TABLEAUX 2019

Y2 - 3 September 2019 through 5 September 2019

ER -