Proof systems: from nestings to sequents and back
classification
💻 cs.LO
keywords
systemsnestedlabelledsequentproofalgorithmbackcalculi
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.