<div class="csl-bib-body">
<div class="csl-entry">Lellmann, B., & Pimentel, E. (2019). Modularisation of Sequent Calculi for Normal and Non-normal Modalities. <i>ACM Transactions on Computational Logic</i>, <i>20</i>(2), 1–46. https://doi.org/10.1145/3288757</div>
</div>
-
dc.identifier.issn
1529-3785
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/142657
-
dc.description.abstract
In this work, we explore the connections between (linear) nested sequent calculi and ordinary sequent calculi for normal and non-normal modal logics. By proposing local versions to ordinary sequent rules, we obtain linear nested sequent calculi for a number of logics, including, to our knowledge, the first nested sequent calculi for a large class of simply dependent multimodal logics and for many standard non-normal modal logics. The resulting systems are modular and have separate left and right introduction rules for the modalities, which makes them amenable to specification as bipole clauses. While this granulation of the sequent rules introduces more choices for proof search, we show how linear nested sequent calculi can be restricted to blocked derivations, which directly correspond to ordinary sequent derivations.
en
dc.language.iso
en
-
dc.publisher
ASSOC COMPUTING MACHINERY
-
dc.relation.ispartof
ACM Transactions on Computational Logic
-
dc.subject
Theoretical Computer Science
-
dc.subject
General Computer Science
-
dc.subject
Computational Mathematics
-
dc.subject
Logic
-
dc.subject
modal logic
-
dc.subject
Linear nested sequents
-
dc.subject
labelled systems
-
dc.subject
proof theory
-
dc.title
Modularisation of Sequent Calculi for Normal and Non-normal Modalities