Citations of:
Syntactic Interpolation for Tense Logics and BiIntuitionistic Logic via Nested Sequents
In Maribel Fernandez & Anca Muscholl (eds.), 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Dagstuhl, Germany: pp. 116 (2020)
Add citations
You must login to add citations.


This thesis introduces the "method of structural refinement", which serves as a means of transforming the relational semantics of a modal and/or constructive logic into an 'economical' proof system by connecting two prooftheoretic paradigms: labelled and nested sequent calculi. The formalism of labelled sequents has been successful in that cutfree calculi in possession of desirable prooftheoretic properties can be automatically generated for large classes of logics. Despite these qualities, labelled systems make use of a complicated syntax that explicitly incorporates the (...) 

This paper shows how to derive nested calculi from labelled calculi for propositional intuitionistic logic and firstorder intuitionistic logic with constant domains, thus connecting the general results for labelled calculi with the more refined formalism of nested sequents. The extraction of nested calculi from labelled calculi obtains via considerations pertaining to the elimination of structural rules in labelled derivations. Each aspect of the extraction process is motivated and detailed, showing that each nested calculus inherits favorable prooftheoretic properties from its associated (...) 

This paper studies the relationship between labelled and nested calculi for propositional intuitionistic logic, firstorder intuitionistic logic with nonconstant domains and firstorder intuitionistic logic with constant domains. It is shown that Fitting’s nested calculi naturally arise from their corresponding labelled calculi—for each of the aforementioned logics—via the elimination of structural rules in labelled derivations. The translational correspondence between the two types of systems is leveraged to show that the nested calculi inherit prooftheoretic properties from their associated labelled calculi, such as (...) 