Mathematician and logician Gerhard Gentzen introduced sequent calculus, a logical framework, in the first half of the 20th century. It can be used to establish systems for propositional, first-order, and modal logics. For the latter, it has some shortcomings. Several structural modifications and extensions have been proposed to improve the handling of modalities. Nested sequents and labeled sequents are two examples.

The authors examine linear nested sequents (LNS). This is a linear variant of the more general treelike nested sequents. It is obtained by adding a nesting operator to the sequent calculus that corresponds structurally to the box modality. The LNS framework is used as a modular way to obtain systems for different normal modal logics, multimodal logics, and non-normal modal logics. It provides left-hand and right-hand rules for modalities, with only a bounded number of principal formulae in each rule. A downside of the modularity of this approach is an increased number of rules, and thereby an increased complexity in proof derivation. This issue is addressed by establishing a normal form for derivations.

This paper assumes familiarity with sequent calculus and modal logic. Given this prerequisite, the paper is self-contained and provides all definitions and soundness and completeness proofs, as well as a few examples. The authors also include a thorough list of references. This paper can serve as a starting point in the field of LNS and other extensions of sequent calculus for modal logics.