Article contents
CUT ELIMINATION IN HYPERSEQUENT CALCULUS FOR SOME LOGICS OF LINEAR TIME
Published online by Cambridge University Press: 13 August 2019
Abstract
This is a sequel article to [10] where a hypersequent calculus (HC) for some temporal logics of linear frames including Kt4.3 and 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.
- Type
- Research Article
- Information
- Copyright
- Copyright © Association for Symbolic Logic 2019
References
BIBLIOGRAPHY
- 2
- Cited by