Indexed systems of sequents and cut-elimination (Q1372944)

The author presents a detailed proof of cut-elimination applied to systems of indexed sequents for all propositional modal logics obtained from the smallest normal modal logic by adding the reflexivity, symmetry and transitivity axioms. Moreover, it is shown how these systems of indexed sequents can be translated into theorem-wise equivalent display sequent calculi as developed by \textit{N. D. Belnap} [see, e.g., Notre Dame J. Formal Logic 31, 14-25 (1990; Zbl 0706.03043); H. Wansing (ed.), Proof theory of modal logic, Proc. Workshop, Hamburg 1993, Appl. Log. Ser. 2, 79-92 (1996; Zbl 0867.03017)].