Abstract

This is a sequel article to [10] where a hypersequent calculus for some temporal logics of linear frames includingKt4.3and its extensions for dense and serial flow of time was investigated in detail. A distinctive feature of this approach is that hypersequents are noncommutative, i.e., they are finite lists of sequents in contrast to other hypersequent approaches using sets or multisets. Such a system in [10] was proved to be cut-free HC formalization of respective logics by means of semantical argument. In this article we present an equivalent variant of this calculus for which a constructive syntactical proof of cut elimination is provided.