Linear nested sequents, 2-sequents and hypersequents

Abstract

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.