Linear Nested Sequents, 2-Sequents and Hypersequents

We introduce the framework of linear nested sequent calculi by restricting nested sequents to linear structures. We show the close connection between this framework and that of 2-sequents, and provide linear nested sequent calculi for a number of modal logics as well as for intuitionistic logic. Furthermore, we explore connections to backwards proof search for sequent calculi and to the hypersequent framework, including a reinterpretation of various hypersequent calculi for modal logic S5 in the linear nested sequent framework.