Pokaż uproszczony rekord

Unified Sequent Calculi and Natural Deduction Systems for Until-free Linear-time Temporal Logics

dc.contributor.authorKamide, Norihiro
dc.contributor.authorNegri, Sara
dc.date.accessioned2025-12-12T15:22:21Z
dc.date.available2025-12-12T15:22:21Z
dc.date.issued2025-11-27
dc.identifier.issn0138-0680
dc.identifier.urihttp://hdl.handle.net/11089/56967
dc.description.abstractA unified Gentzen-style proof-theoretic framework for until-free propositional linear-time temporal logic and its intuitionistic variant is introduced. The framework unifies Gentzen-style single-succedent sequent calculi and natural deduction systems for both the classical and intuitionistic versions of these temporal logics. Theorems establishing the equivalence between the proposed sequent calculi and natural deduction systems are proved. Furthermore, the cut-elimination theorems for the proposed sequent calculi and the normalization theorems for the proposed natural deduction systems are established.en
dc.language.isoen
dc.publisherWydawnictwo Uniwersytetu Łódzkiegopl
dc.relation.ispartofseriesBulletin of the Section of Logic;2en
dc.rights.urihttps://creativecommons.org/licenses/by-nc-nd/4.0
dc.subjectlinear-time temporal logicen
dc.subjectintuitionistic linear-time temporal logicen
dc.subjectsequent calculusen
dc.subjectnatural deductionen
dc.subjectcut-elimination theoremen
dc.subjectnormalization theoremen
dc.titleUnified Sequent Calculi and Natural Deduction Systems for Until-free Linear-time Temporal Logicsen
dc.typeArticle
dc.page.number227-282
dc.contributor.authorAffiliationKamide, Norihiro - Nagoya City University, School of Data Scienceen
dc.contributor.authorAffiliationNegri, Sara - University of Genoa, Department of Mathematicsen
dc.identifier.eissn2449-836X
dc.referencesA. Abuin, A. Bolotov, M. Hermo, P. Lucio, Tableaux and sequent calculi for CTL and ECTL: Satisfiability test with certifying proofs and models, Journal of Logical and Algebraic Methods in Programming 130, 100828, (2023), DOI: https://doi.org/10.1016/J.JLAMP.2022.100828en
dc.referencesA. Almukdad, D. Nelson, Constructible falsity and inexact predicates, Journal of Symbolic Logic, vol. 49(1) (1984), pp. 231–233, DOI: https://doi.org/10.2307/2274105en
dc.referencesS. Baratella, A. Masini, A proof-theoretic investigation of a logic of positions, Annals of Pure and Applied Logic, vol. 123 (2003), pp. 135–162, DOI: https://doi.org/10.1016/S0168-0072(03)00021-6en
dc.referencesS. Baratella, A. Masini, An approach to infinitary temporal proof theory, Archive for Mathematical Logic, vol. 43(8) (2004), pp. 965–990, DOI: https://doi.org/10.1007/S00153-004-0237-Zen
dc.referencesZ.-E.-A. Benaissa, E. Moggi, W. Taha, T. Sheard, Logical modalities and multi-stage programming, [in:] Proceedings of Workshop on Intuitionistic Modal Logics and Applications (IMLA’99) (1999), 15 pp.en
dc.referencesA. Bolotov, A. Basukoski, O. M. Grigoriev, V. Shangin, Natural deduction calculus for linear-time temporal logic, [in:] Proceedings of the 10th European Conference on Logics in Artificial Intelligence (JELIA 2006), vol. 4160 of Lecture Notes in Computer Science (2006), pp. 56–68, DOI: https://doi.org/10.1007/11853886_7en
dc.referencesA. Bolotov, V. Shangin, Natural deduction system in paraconsistent setting: Proof search for PCont, Journal of Intelligent Systems, vol. 21(1) (2012), pp. 1–24, DOI: https://doi.org/10.1515/JISYS-2011-0021en
dc.referencesB. Boretti, S. Negri, Decidability for Priorean linear time using a fixed-point labelled calculus, [in:] Proceedings of the 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), vol. 5607 of Lecture Notes in Computer Science (2009), pp. 108–122, DOI: https://doi.org/10.1007/978-3-642-02716-1_9en
dc.referencesB. Boretti, S. Negri, On the finitization of Priorean linear time, [in:] M. D’Agostino, G. Giorello, F. Laudisa, T. Pievani, C. Sinigaglia (eds.), New Essays in Logic and Philosophy of Science, College Publications, London (2010), pp. 67–79.en
dc.referencesK. Brünnler, M. Lange, Cut-free sequent systems for temporal logic, Journal of Logical and Algebraic Methods in Programming, vol. 76(2) (2008), pp. 216–225, DOI: https://doi.org/10.1016/J.JLAP.2008.02.004en
dc.referencesS. Cerrito, V. Goranko, S. Paillocher, Partial model checking and partial model synthesis in LTL using a Tableau-based approach, [in:] Proceedings of the 8th International Conference on Formal Structures for Computation and Deduction (FSCD) (2023), pp. 23:1–23:21, DOI: https://doi.org/10.4230/LIPICS.FSCD.2023.23en
dc.referencesR. Davies, A Temporal-Logic Approach to Binding-Time Analysis, [in:] Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS), IEEE Computer Society (1996), pp. 184–195, DOI: https://doi.org/10.1109/LICS.1996.561317en
dc.referencesR. Davies, F. Pfenning, A modal analysis of staged computation, Journal of the ACM, vol. 48(3) (2001), pp. 555–604, DOI: https://doi.org/10.1145/382780.382785en
dc.referencesE. A. Emerson, Temporal and modal logic, Elsevier and MIT Press (1990), pp. 995–1072, DOI: https://doi.org/10.1016/B978-0-444-88074-1.50021-4en
dc.referencesJ. Gaintzarain, M. Hermo, P. Lucio, M. Navarro, F. Orejas, A cut-free and invariant-free sequent calculus for PLTL, vol. 4646 of Lecture Notes in Computer Science, Springer (2007), pp. 481–495, DOI: https://doi.org/10.1007/978-3-540-74915-8_36en
dc.referencesY. Gurevich, Intuitionistic logic with strong negation, Studia Logica, vol. 36 (1977), pp. 49–59.en
dc.referencesS. Huang, R. Cleaveland, A tableau construction for finite linear-time temporal logic, Journal of Logical and Algebraic Methods in Programing, vol. 125 (2022), p. 100743, DOI: https://doi.org/10.1016/J.JLAMP.2021.100743en
dc.referencesN. Kamide, An equivalence between sequent calculi for linear-time temporal logic, Bulletin of the Section of Logic, vol. 35(4) (2006), pp. 187–194.en
dc.referencesN. Kamide, Embedding Linear-Time Temporal Logic into Infinitary Logic: Application to Cut-Elimination for Multi-agent Infinitary Epistemic Linear-Time Temporal Logic, [in:] M. Fisher, F. Sadri, M. Thielscher (eds.), Computational Logic in Multi-Agent Systems, Springer Berlin Heidelberg, Berlin, Heidelberg (2009), pp. 57–76, DOI: https://doi.org/10.1007/978-3-642-02734-5_5en
dc.referencesN. Kamide, Notes on an extension of Davies’ logic for binding-time analysis, Far East Journal of Applied Mathematics, vol. 44(1) (2010), pp. 37–57.en
dc.referencesN. Kamide, Bounded linear-time temporal logic: A proof-theoretic investigation, Annals of Pure and Applied Logic, vol. 163(4) (2012), pp. 439–466, DOI: https://doi.org/10.1016/J.APAL.2011.12.002en
dc.referencesN. Kamide, Temporal Gödel-Gentzen and Girard translations, Mathematical Logic Quarterly, vol. 59(1–2) (2013), pp. 66–83, DOI: https://doi.org/10.1002/MALQ.201100083en
dc.referencesN. Kamide, Embedding theorems for LTL and its variants, Mathematical Structures in Computer Science, vol. 25(1) (2015), pp. 83–134, DOI: https://doi.org/10.1017/S0960129514000048en
dc.referencesN. Kamide, Interpolation theorems for some variants of LTL, Reports on Mathematical Logic, vol. 50 (2015), pp. 3–30, URL: https://rml.tcs.uj.edu.pl/rml-50/1-kamide.pdfen
dc.referencesN. Kamide, Relating first-order monadic omega-logic, propositional linear-time temporal logic, propositional generalized definitional reflection logic and propositional infinitary logic, Journal of Logic and Computation, vol. 27(7) (2017), pp. 2271–2301, DOI: https://doi.org/10.1093/LOGCOM/EXX006en
dc.referencesN. Kamide, Natural deduction with explosion and excluded middle, [in:] Proceedings of the 53rd IEEE International Symposium on Multiple-valued Logic (ISMVL 2023) (2023), pp. 24–29, DOI: https://doi.org/10.1109/ISMVL57333.2023.00016en
dc.referencesN. Kamide, Refutation-Aware Gentzen-Style Calculi for Propositional Until-Free Linear-Time Temporal Logic, Studia Logica, vol. 111(6) (2023), pp. 979–1014, DOI: https://doi.org/10.1007/S11225-023-10052-7en
dc.referencesN. Kamide, S. Negri, A unified Gentzen-style framework for until-free LTL, vol. 415 of Electronic Proceedings in Theoretical Computer Science (2024), pp. 165–179, DOI: https://doi.org/10.4204/EPTCS.415.16en
dc.referencesN. Kamide, S. Negri, Proof theory for extended Belnap–Dunn and intuitionistic logics, Studia Logica, (2025), DOI: https://doi.org/10.1007/s11225-025-10203-y online first.en
dc.referencesN. Kamide, S. Negri, Unified natural deduction for logics of strong negation, Notre Dame Journal of Formal Logic, vol. 66(4) (2025), pp. 543–580, DOI: https://doi.org/10.1215/00294527-2025-0016en
dc.referencesN. Kamide, H. Wansing, Combining linear-time temporal logic with constructiveness and paraconsistency, Journal of Applied Logic, vol. 8(1) (2011), pp. 33–61, DOI: https://doi.org/10.1016/J.JAL.2009.06.001en
dc.referencesN. Kamide, H. Wansing, A paraconsistent linear-time temporal logic, Fundamenta Informaticae, vol. 106(1) (2011), pp. 1–23, DOI: https://doi.org/10.3233/FI-2011-374en
dc.referencesH. Kawai, Sequential calculus for a first order infinitary temporal logic, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 33 (1987), pp. 423–432, DOI: https://doi.org/10.1002/MALQ.19870330506en
dc.referencesI. Kim, K. Yi, C. Calcagno, A polymorphic modal type system for lisp-like multi-staged languages, [in:] J. G. Morrisett, S. L. P. Jones (eds.), Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), ACM (2006), pp. 257–268, DOI: https://doi.org/10.1145/1111037.1111060en
dc.referencesK. Kojima, A. Igarashi, On constructive linear-time temporal logic, [in:] Proceedings of Intuitionistic Modal Logics and Applications Workshop (IMLA’08) (2008), 12 pp.en
dc.referencesN. Kürbis, Y. Petrukhin, Normalisation for some quite interesting many-valued logics, Logic and Logical Philosophy, vol. 30(3) (2021), pp. 493–534.en
dc.referencesE. Moggi, W. Taha, Z.-E.-A. Benaissa, T. Sheard, An Idealized MetaML: Simpler, and More Expressive, [in:] S. D. Swierstra (ed.), Proceedings of the 8th European Symposium on Programming (ESOP’99), vol. 1576 of Lecture Notes in Computer Science, Springer (1999), pp. 193–207, DOI: https://doi.org/10.1007/3-540-49099-X_13en
dc.referencesA. Nanevski, Meta-programming with names and necessity, [in:] M. Wand, S. L. P. Jones (eds.), Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP ’02), ACM (2002), pp. 206–217, DOI: https://doi.org/10.1145/581478.581498en
dc.referencesS. Negri, Geometric rules in infinitary logic, [in:] O. Arieli, A. Zamansky (eds.), Arnon Avron on Semantics and Proof Theory of Non-Classical Logics, Outstanding Contributions to Logic, Springer (2021), pp. 265–293en
dc.referencesS. Negri, J. von Plato, Sequent calculus in natural deduction style, Journal of Symbolic Logic 66 (4), (2001), pp. 1803–1816, DOI: https://doi.org/10.2307/2694976en
dc.referencesS. Negri, J. von Plato, Structural Proof Theory (2001), DOI: https://doi.org/10.1017/CBO9780511527340en
dc.referencesD. Nelson, Constructible falsity, Journal of Symbolic Logic, vol. 14 (1949), pp. 16–26, DOI: https://doi.org/10.2307/2268973en
dc.referencesB. Paech, Gentzen-Systems for propositional temporal logics, [in:] E. Börger, H. K. Büning, M. M. Richter (eds.), CSL ’88, Springer Berlin Heidelberg, Berlin, Heidelberg (1989), pp. 240–253, DOI: https://doi.org/10.1007/BFb0026305en
dc.referencesR. Pliuškevičius, Investigation of finitary calculus for a discrete linear time logic by means of infinitary calculus, [in:] J. Bārzdinš, D. Bjørner (eds.), Baltic Computer Science, Springer Berlin Heidelberg, Berlin, Heidelberg (1991), pp. 504–528, DOI: https://doi.org/10.1007/BFb0019366en
dc.referencesA. Pnueli, The temporal logic of programs (1977), pp. 46–57, DOI: https://doi.org/10.1109/SFCS.1977.32en
dc.referencesD. Prawitz, Natural deduction: a proof-theoretical study (1965), DOI: https://doi.org/10.2307/2271676en
dc.referencesG. Priest, Natural Deduction Systems for Logics in the FDE Family, [in:] H. Omori, H. Wansing (eds.), New Essays on Belnap-Dunn Logic, Springer International Publishing, Cham (2019), pp. 279–292, DOI: https://doi.org/10.1007/978-3-030-31136-0_16en
dc.referencesM. E. Szabo, Collected papers of Gerhard Gentzen, [in:] M. E. Szabo (ed.), Studies in Logic and the Foundations of Mathematics, North-Holland (1969), DOI: https://doi.org/10.2307/2272429 english translation.en
dc.referencesM. E. Szabo, A sequent calculus for Kröger logic, [in:] A. Salwicki (ed.), Logics of Programs and Their Applications, Springer Berlin Heidelberg, Berlin, Heidelberg (1983), pp. 295–303, DOI: https://doi.org/10.1007/3-540-11981-7_21en
dc.referencesW. Taha, T. Sheard, Multi-Stage Programming with Explicit Annotations, [in:] J. P. Gallagher, C. Consel, A. M. Berman (eds.), Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM ’97), ACM (1997), pp. 203–217, DOI: https://doi.org/10.1145/258993.259019en
dc.referencesL. Tranchini, Natural deduction for bi-intuitionistic logic, Journal of Applied Logic, vol. 25(Supplement) (2017), pp. S72–S96, DOI: https://doi.org/10.1016/J.JAL.2017.12.001en
dc.referencesA. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, vol. 45 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, (2000), DOI: https://doi.org/10.1017/CBO9781139168717en
dc.referencesJ. von Plato, Proof theory of full classical propositional logic (1999), manuscript, 16 pp.en
dc.referencesJ. von Plato, Elements of Logical Reasoning (2014), DOI: https://doi.org/10.1017/CBO9781139567862en
dc.referencesJ. von Plato, Saved from the Cellar: Gerhard Gentzen’s Shorthand Notes on Logic & Foundations of Mathematics (2017), DOI: https://doi.org/10.1007/978-3-319-42120-9en
dc.referencesY. Yuse, A. Igarashi, A modal type system for multi-level generating extensions with persistent code, [in:] A. Bossi, M. J. Maher (eds.), Proceedings of the 8th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, ACM (2006), pp. 201–212, DOI: https://doi.org/10.1145/1140335.1140360en
dc.contributor.authorEmailKamide, Norihiro - drnkamide08@kpd.biglobe.ne.jp
dc.contributor.authorEmailNegri, Sara - sara.negri@unige.it
dc.identifier.doi10.18778/0138-0680.2025.09
dc.relation.volume54


Pliki tej pozycji

Thumbnail
Nazwa:
227-282_Kamide_et_al..pdf
Rozmiar:
1.548MB
Format:
PDF
Oglądaj/Otwórz

Pozycja umieszczona jest w następujących kolekcjach

Pokaż uproszczony rekord

https://creativecommons.org/licenses/by-nc-nd/4.0
Poza zaznaczonymi wyjątkami, licencja tej pozycji opisana jest jako https://creativecommons.org/licenses/by-nc-nd/4.0