Eliminability of cut in hypersequent calculi for some modal logics of linear frames (Q477584)

The paper presents Avron-style hypersequent calculi for the modal logics of linear frames K4.3, D4.3, and S4.3 and gives a constructive syntactic proof that they satisfy cut elimination. A form of the calculus for S4.3 appeared in an earlier paper by the author [Bull. Sect. Log., Univ. Łódź, Dep. Log. 41, No. 1--2, 89--104 (2012; Zbl 1287.03046)], but only with a semantic proof of cut elimination (i.e., completeness of the cut-free system). The cut elimination proof in the present paper is based on the method of \textit{A. Ciabattoni} et al. [Fuzzy Sets Syst. 161, No. 3, 369--389 (2010; Zbl 1190.03026)].