Hostname: page-component-78c5997874-g7gxr Total loading time: 0 Render date: 2024-11-19T15:33:03.615Z Has data issue: false hasContentIssue false
  • English
  • Français

CUT ELIMINATION IN HYPERSEQUENT CALCULUS FOR SOME LOGICS OF LINEAR TIME

Published online by Cambridge University Press:  13 August 2019

ANDRZEJ INDRZEJCZAK
ANDRZEJ INDRZEJCZAK*
Affiliation:
Department of Logic, Institute of Philosophy, University of Lodz
*
*DEPARTMENT OF LOGIC INSTITUTE OF PHILOSOPHY UNIVERSITY OF LODZ LINDLEYA 3/5, 90–131 ŁÓDŹ POLAND E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

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.

Keywords

03B4403F0303F05temporal logichypersequent calculuscut elimination
Type
Research Article
Information
The Review of Symbolic Logic , Volume 12 , Issue 4 , December 2019 , pp. 806 - 822
Copyright
Copyright © Association for Symbolic Logic 2019 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

BIBLIOGRAPHY

Avron, A. (1987). A constructive analysis of RM. Journal of Symbolic Logic, 52, 939–951.CrossRefGoogle Scholar
Avron, A. (1991). Using hypersequents in proof systems for nonclassical logics. Annals of Mathematics and Artificial Intelligence, 4, 225–248.CrossRefGoogle Scholar
Avron, A. (1996). The method of hypersequents in the proof theory of logic. In Hodges, W., Hyland, M., Steinhorn, C., and Truss, J., editors. Logic: From Foundations to Applications. Oxford: Oxford Science Publication, pp. 225–248.Google Scholar
Baaz, M., Ciabattoni, A., & Fermüller, C. (2003). Hypersequent calculi for Gödel logics—A survey. Journal of Logic and Computation, 13, 1–27.CrossRefGoogle Scholar
Baelde, D., Lick, A., & Schmitz, S. (2018). A hypersequent calculus with clusters for linear frames. In Bezhanishvili, G., D’Agostino, G., Metcalfe, G., and Studer, T., editors. Advances in Modal Logic, Vol. 12. London: College Publications, pp. 43–62.Google Scholar
Bednarska, K., & Indrzejczak, A. (2015). Hypersequent calculi for S5—The methods of cut-elimination. Logic and Logical Philosophy, 24(3), 277–311.Google Scholar
Ciabattoni, A., Metcalfe, G., & Montagna, F. (2010). Algebraic and proof-theoretic characterizations of truth stressers for mtl and its extensions. Fuzzy Sets and Systems, 161(3), 369–389.CrossRefGoogle Scholar
Indrzejczak, A. (2012). Cut-free hypersequent calculus for S4.3. Bulletin of the Section of Logic, 41(1–2), 89–104.Google Scholar
Indrzejczak, A. (2015). Eliminability of cut in hypersequent calculi for some modal logics of linear frames. Information Processing Letters, 115(2), 75–81.CrossRefGoogle Scholar
Indrzejczak, A. (2016). Linear time in hypersequent framework. The Bulletin of Symbolic Logic, 22(1), 121–144.CrossRefGoogle Scholar
Indrzejczak, A. (2017). Cut elimination theorem for noncommutative hypersequent calculus. Bulletin of the Section of Logic, 46(1–2), 135–149.Google Scholar
Kurokawa, H. (2014). Hypersequent calculi for modal logics extending S4. In Nakano, Y., Satoh, K., and Bekki, D., editors. New Frontiers in Artificial Intelligence (2013). Cham: Springer, pp. 51–68.CrossRefGoogle Scholar
Kuznets, R. & Lellmann, B. (2016). Grafting hypersequents onto nested sequents. Logic Journal of the IGPL, 24(3), 375–423.CrossRefGoogle Scholar
Lahav, O. (2013). From frame properties to hypersequent rules in modal logics. In Kupferman, O., editor. Proceedings of LICS. Washington, DC: IEEE Computer Society Press, pp. 408–417.Google Scholar
Lellmann, B. (2014). Axioms vs hypersequent rules with context restrictions. In Demri, S., Kapur, D., and Weidenbech, C., editors. Proceedings of IJCAR. Cham: Springer, pp. 307–321.Google Scholar
Lellmann, B. (2015). Linear nested sequents, 2-sequents and hypersequents. In de Nivelle, H., editor. TABLEAUX. Cham: Springer, pp. 135–150.Google Scholar
Metcalfe, G., Olivetti, N., & Gabbay, D. (2008). Proof Theory for Fuzzy Logics. Cham: Springer.Google Scholar
Mints, G. (1968). Some calculi of modal logic. Trudy Matematicheskogo Instituta imeni V. A. Steklova, 98, 88–111.Google Scholar
Pottinger, G. (1983). Uniform cut-free formulations of T, S4, and S5 (abstract). Journal of Symbolic Logic, 48, 900.Google Scholar
Schütte, K. (1977). Proof Theory. Berlin: Springer.CrossRefGoogle Scholar