The method of tree-hypersequents for modal propositional logic
pp. 31-51
in: David Makinson, Jacek Malinowski, Heinrich Wansing (eds), Towards mathematical philosophy, Berlin, Springer, 2009Abstract
In this paper we present a method, that we call the tree-hypersequent method, for generating contraction-free and cut-free sequent calculi for modal propositional logics. We show how this method works for the systems K, KD, K4 and KD4, by giving a sequent calculus for these systems which are normally presented in the Hilbert style, and by proving all the main results in a purely syntactical way.