Proof systems: from nestings to sequents and back
Logic in Computer Science
2018-02-15 v2
Abstract
In this work, we explore proof theoretical connections between sequent, nested and labelled calculi. In particular, we show a general algorithm for transforming a class of nested systems into sequent calculus systems, passing through linear nested systems. Moreover, we show a semantical characterisation of intuitionistic, multi-modal and non-normal modal logics for all these systems, via a case-by-case translation between labelled nested to labelled sequent systems.
Keywords
Cite
@article{arxiv.1802.04704,
title = {Proof systems: from nestings to sequents and back},
author = {Elaine Pimentel},
journal= {arXiv preprint arXiv:1802.04704},
year = {2018}
}
Comments
Extended version of the paper submitted to IJCAR-18