Sequentialising Nested Systems

Elaine Pimentel*, Revantha Ramanayake, Björn Lellmann

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

3 Citations (Scopus)


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 languageEnglish
Title of host publicationAutomated Reasoning with Analytic Tableaux and Related Methods
EditorsSerenella Cerrito, Andrei Popescu
Number of pages19
ISBN (Electronic)978-3-030-29026-9
ISBN (Print)978-3-030-29025-2
Publication statusPublished - 2019
Externally publishedYes
Event28th International Conference, TABLEAUX 2019 - London, United Kingdom
Duration: 3-Sep-20195-Sep-2019


Conference28th International Conference, TABLEAUX 2019
Country/TerritoryUnited Kingdom

Cite this