Citations of:
Add citations
You must login to add citations.


We employ a recently developed methodology  called "structural refinement"  to extract nested sequent systems for a sizable class of intuitionistic modal logics from their respective labelled sequent systems. This method can be seen as a means by which labelled sequent systems can be transformed into nested sequent systems through the introduction of propagation rules and the elimination of structural rules, followed by a notational translation. The nested systems we obtain incorporate propagation rules that are parameterized with formal grammars, (...) 

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 (...) 