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)

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

Conference

Conference28th International Conference, TABLEAUX 2019
Country/TerritoryUnited Kingdom
CityLondon
Period03/09/201905/09/2019

Cite this