Cut Elimination Theorem for Non-Commutative Hypersequent Calculus

• Autorzy: Andrzej Indrzejczak
• Języki publikacji: EN

Abstrakty

EN

Hypersequent calculi (HC) can formalize various non-classical logics. In [9] we presented a non-commutative variant of HC for the weakest temporal logic of linear frames Kt4.3 and some its extensions for dense and serial flow of time. The system was proved to be cut-free HC formalization of respective temporal logics by means of Schütte/Hintikka-style semantical argument using models built from saturated hypersequents. In this paper we present a variant of this calculus for Kt4.3 with a constructive syntactical proof of cut elimination.

Słowa kluczowe

EN

temporal logic; linear time; hypersequent calculus; cut elimination

• Wydawca: Wydawnictwo Uniwersytetu Łódzkiego
• Czasopismo: Bulletin of the Section of Logic
• Rocznik: 2017
• Tom: 46
• Numer: 1/2

Daty

wydano

2017-06-30

Twórcy

autor

Andrzej Indrzejczak

• University of Łódź, Department of Logic, Lindleya 3/5, Łódź

Bibliografia

• [1] A. Avron, A Constructive Analysis of RM, Journal of Symbolic Logic 52 (1987), pp. 939–951.
• [2] A. Avron, Using Hypersequents in Proof Systems for Non-Classical Logics, Annals of Mathematics and Artificial Intelligence 4 (1991), pp. 225–248.
• [3] A. Avron, The Method of Hypersequents in the Proof Theory of Propositional Non-Classical Logics, [in:] W. Hodges et al. (eds.), Logic: From Foundations to Applications, Oxford Science Publication, Oxford, 1996, pp. 1–32.
• [4] M. Baaz, A. Ciabattoni and C. G. Fermüller, Hypersequent Calculi for Gödel Logics – a Survey, Journal of Logic and Computation 13 (2003), pp. 1–27.
• [5] K. Bednarska and A. Indrzejczak, Hypersequent Calculi for S5 – the Methods of Cut-elimination, Logic and Logical Philosophy 24/3 (2015), pp. 277–311.
• [6] A. Ciabattoni, N. Galatos and K. Terui, From axioms to analytic rules in nonclassical logics, LICS (2008), pp. 229–240.
• [7] A. Indrzejczak, Cut-free Hypersequent Calculus for S4.3, Bulletin of the Section of Logic 41:1/2 (2012), pp. 89–104.
• [8] A. Indrzejczak, Eliminability of Cut in Hypersequent Calculi for some Modal Logics of Linear Frames, Information Processing Letters 115/2 (2015), pp. 75–81.
• [9] A. Indrzejczak, Linear Time in Hypersequent Framework, The Bulletin of Symbolic Logic 22/1 (2016), pp. 121–144.
• [10] O. Lahav, From Frame Properties to Hypersequent Rules in Modal Logics, LICS 2013.
• [11] B. Lellmann, Axioms vs hypersequent rules with context restrictions, [in:] Proceedings of IJCAR, Springer 2014, pp. 307–321.
• [12] B. Lellmann, Linear Nested Sequents, 2-Sequents and Hypersequents, [in:] TABLEAUX, Springer 2015, pp. 135–150.
• [13] H. Kurokawa, Hypersequent Calculi for Modal Logics Extending S4, [in:] New Frontiers in Artificial Intelligence (2013), pp. 51–68, Springer, 2014.
• [14] G. Metcalfe, N. Olivetti and D. Gabbay, Proof Theory for Fuzzy Logics, Springer 2008.
• [15] F. Poggiolesi, A Cut-free Simple Sequent Calculus for Modal Logic S5, Review of Symbolic Logic 1 (2008), pp. 3–15.
• [16] F. Poggiolesi, Gentzen Calculi for Modal Propositional Logics, Springer, 2011.
• [17] G. Pottinger, Uniform Cut-free formulations of T, S4 and S5 (abstract), Journal of Symbolic Logic 48 (1983), p. 900.
• [18] K. Schütte, Proof Theory, Springer, 1977.

Identyfikatory

DOI

10.18778/0138-0680.46.1.2.10