Abstract
This study introduces refutation-aware Gentzen-style sequent calculi and Kripke-style semantics for propositional until-free linear-time temporal logic. The sequent calculi and semantics are constructed on the basis of the refutation-aware setting for Nelson’s paraconsistent logic. The cut-elimination and completeness theorems for the proposed sequent calculi and semantics are proven.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Abadi, M., and Z. Manna, Nonclausal deduction in first-order temporal logic, Journal of the ACM 37 (2): 279–317, 1990.
Almukdad, A., and D. Nelson, Constructible falsity and inexact predicates, Journal of Symbolic Logic 49 (1): 231–233, 1984.
Baratella, S., and A. Masini, An approach to infinitary temporal proof theory, Archive for Mathematical Logic 43 (8): 965–990, 2004.
Belnap, N. D., A useful four-valued logic, in: G. Epstein, and J. M. Dunn, (eds.), Modern Uses of Multiple-Valued Logic, Dordrecht, Reidel, 1977, pp. 5–37.
Belnap, N. D., How a computer should think, in: G. Ryle, (ed.), Contemporary Aspects of Philosophy, Oriel Press, Stocksfield, 1977, pp. 30–56.
Brünnler, K., and M. Lange, Cut-free sequent systems for temporal logic, Journal of Logic and Algebraic Methods in Programming 76 (2): 216–225, 2008.
Cavalli, A. R., and L. Fariñas del Cerro, A Decision Method for Linear Temporal Logic, vol. 170 of Lecture Notes in Computer Science, 1984, pp. 113–127.
Clarke, E. M., and E. A. Emerson, Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic, vol. 131 of Lecture Notes in Computer Science, 1981, pp. 52–71.
Clarke, E. M., O. Grumberg, S. Jha, Y. Lu, and H. Veith, Counterexample-guided abstraction refinement for symbolic model checking, Journal of the ACM 50 (5): 752–794, 2003.
Clarke, E. M., T. A. Henzinger, H. Veith, and R. Bloem, (eds.), Handbook of Model Checking, Springer, 2018.
Czermak, J., A remark on Gentzen’s calculus of sequents, Notre Dame Journal of Formal Logic 18: 471–474, 1977.
Degtyarev, A., M. Fisher, and B. Konev, Monodic temporal resolution, ACM Transaction on Computational Logic 7 (1): 108–150, 2006.
Dixon, C., Temporal resolution using a breadth-first search algorithm, Annals of Mathematics and Artificial Intelligence 22: 87–115, 1998.
Dunn, J. M., Intuitive semantics for first-degree entailment and ‘coupled trees’, Philosophical Studies 29 (3): 149–168, 1976.
Emerson, E. A., Temporal and modal logic, in: J. van Leeuwen, (ed.), Handbook of Theoretical Computer Science, Formal Models and Semantics (B), Elsevier and MIT Press, 1990, pp. 995–1072.
Fisher, M., A resolution method for temporal logic, in Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI), 1991, pp. 99–104.
Fisher, M., C. Dixon, and M. Peim, Clausal temporal resolution, ACM Transactions on Computational Logic 2 (1): 12–56, 2001.
Gaintzarain, J., M. Hermo, P. Lucio, M. Navarro, and F. Orejas, A cut-free and invariant-free sequent calculus for PLTL, in Proceedings of the 21st International Workshop on Computer Science Logic, Lecture Notes in Computer Science 4646, 2008, pp. 481–495.
Gentzen, G., The Collected Papers of Gerhard Gentzen, (english translation), M.E. Szabo, (ed.), vol. 55 of Studies in Logic and the Foundations of Mathematics, North-Holland, 1969.
Goodman, N. D., The logic of contradiction, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 27: 119–126, 1981.
Goranko, V., Refutation systems in modal logic, Studia Logica 53: 299–324, 1994.
Gurfinkel, A., and M. Chechik, Why waste a perfectly good abstraction? in Proceedings of the 12th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2006), vol. 3920 of Lecture Notes in Computer Science, 2006, pp. 212–226.
Gurfinkel, A., O. Wei, and M. Chechik, Yasm: A software model-checker for verification and refutation, in Proceedings of the 18th International Conference on Computer Aided Verification (CAV 2006), 2006, pp. 170–174.
Hodkinson, I., F. Wolter, and M. Zakharyaschev, Decidable fragments of first-order temporal logics, Annals of Pure and Applied Logic 106: 85–134, 2000.
Horn, L. R., and H. Wansing, Negation, in Edward N. Zalta (ed.), The Stanford Encyclopedia of Philosophy (Spring 2017 Edition), Last modified on January 2017, https://plato.stanford.edu/archives/spr2017/entries/negation/.
Hustadt, U., and B. Konev, TRP++2.0: A Temporal Resolution Prover, vol. 2741 of Lecture Notes in Artificial Intelligence, 2003, pp. 274–278.
Kamide, N., Natural deduction systems for Nelson’s paraconsistent logic and its neighbors, Journal of Applied Non-Classical Logics 15 (4): 405–435, 2005.
Kamide, N., An equivalence between sequent calculi for linear-time temporal logic, Bulletin of the Section of the Logic 35 (4): 187–194, 2006.
Kamide, N., A uniform proof-theoretic foundation for abstract paraconsistent logic programming, Journal of Functional and Logic Programming, 1–36, 2007.
Kamide, N., Embedding linear-time temporal logic into infinitary logic: application to cut-elimination for multi-agent infinitary epistemic linear-time temporal logic, in Proceedings of the 9th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA9), vol. 5405 of Lecture Notes in Artificial Intelligence, 2009, pp. 57–76.
Kamide, N., Reasoning about bounded time domain: An alternative to NP-complete fragments of LTL, in Proceedings of the 2nd International Conference on Agents and Artificial Intelligence (ICAART 2010), 2010, pp. 536–539.
Kamide, N., Bounded linear-time temporal logic: A proof-theoretic investigation, Annals of Pure and Applied Logic 163 (4): 439–466, 2012.
Kamide, N., Embedding theorems for LTL and its variants, Mathematical Structures in Computer Science 25 (1): 83–134, 2015.
Kamide, N., 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 27 (7): 2271–2301, 2017.
Kamide, N., Falsification-aware semantics and sequent calculi for classical logic, Journal of Philosophical Logic 51 (1): 99–126, 2022.
Kamide, N., Inconsistency-tolerant hierarchical probabilistic CTL model checking: logical foundations and illustrative examples, International Journal of Software Engineering and Knowledge Engineering 32 (1): 131–162, 2022.
Kamide, N., Falsification-aware semantics for temporal logics and their inconsistency-tolerant subsystems: Theoretical foundations of falsification-aware model checking, International Journal of Software Engineering and Knowledge Engineering 32 (7): 971–1017, 2022.
Kamide, N., and S. Kanbe, Falsification-aware semantics for CTL and its inconsistency-tolerant subsystem: Towards falsification-aware model checking, in Proceedings of the 14th International Conference on Agents and Artificial Intelligence (ICAART 2022), vol. 3, 2022, pp. 242–252.
Kamide, N., and H. Wansing, A paraconsistent linear-time temporal logic, Fundamenta Informaticae 106 (1): 1–23, 2011.
Kamide, N., and H. Wansing, Proof theory of Nelson’s paraconsistent logic: A uniform perspective, Theoretical Computer Science 415: 1–38, 2012
Kamide, N., and H. Wansing, Proof theory of N4-Related Paraconsistent Logics, vol. 54 of Studies in Logic, College Publications, 2015, pp. 1–401.
Kaneiwa, K., and N. Kamide, Paraconsistent computation tree logic, New Generation Computing 29 (4): 391–408, 2011.
Kapsner, A., Logics and Falsifications: A New Perspective on Constructivist Semantics, vol. 40 of Trends in Logic Book, Springer, 2014.
Kawai, H., Sequential calculus for a first order infinitary temporal logic, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 33: 423–432, 1987.
Lichtenstein, O., and A. Pnueli, Propositional temporal logics: decidability and completeness, Logic Journal of the IGPL 8 (1): 55–85, 2000.
Łukasiewicz, J., Aristotle’s Syllogistic from the Standpoint of Modern Formal Logic, Oxford, 1951 (Aristotle’s Syllogistic from the Standpoint of Modern Formal Logic - Greek & Roman philosophy, Taylor & Francis, 1987).
Łukowski, P., A deductive-reductive form of logic: General theory and intuitionistic case, Logic and Logical Philosophy 10: 59–78, 2002.
Miller, D., G. Nadathur, F. Pfenning, and A. Scedrov, Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic 51: 125–157, 1991.
Nelson, D., Constructible falsity, Journal of Symbolic Logic 14: 16–26, 1949.
Paech, B., Gentzen-Systems for Propositional Temporal Logics, vol. 385 of Lecture Notes in Computer Science, 1988, pp. 240–253.
Pliuškevičius, R., Investigation of Finitary Calculus for a Discrete Linear Time Logic by Means of Infinitary Calculus, vol. 502 of Lecture Notes in Computer Science, 1991, pp. 504–528.
Pnueli, A., The temporal logic of programs, in Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, 1977, pp. 46–57.
Priest, G., and K. Tanaka, Paraconsistent logic, in: E. N. Zalta (ed.), The Stanford Encyclopedia of Philosophy (Summer 2009 Edition), http://plato.stanford.edu/archives/sum2009/entries/logic-paraconsistent/
Rauszer, C., A formalization of the propositional calculus of H-B logic, Studia Logica 33: 23–34, 1974.
Rauszer, C., Applications of Kripke models to Heyting-Brouwer logic, Studia Logica 36: 61–71, 1977.
Rauszer, C., An Algebraic and Kripke-Style Approach to a Certain Extension of Intuitionistic Logic, Dissertations Mathematicae, Polish Scientific Publishers, 1980, pp. 1–67.
Robinson, J. A., A machine-oriented logic based on the resolution principle, Journal of the ACM, 12 (1): 23–41, 1965.
Sakuragawa, T., Temporal Prolog: a programming language based on temporal logic, Computer Software 4 (3): 199–211, 1987.
Shramko, Y., Dual intuitionistic logic and a variety of negations: The logic of scientific research, Studia Logica 80 (2–3): 347–367, 2005.
Shramko, Y., A modal translation for dual-intuitionistic logic, Review of Symbolic Logic 9 (2): 251–265, 2016.
Skura, T. F., A Łukasiewicz-style refutation system for the modal logic S4, Journal of Philosophical Logic 24: 573–582, 1995.
Skura, T. F., Refutations, proofs, and models in the modal logic K4, Studia Logica 70 (2): 193–204, 2002.
Skura, T. F., Refutation systems in propositional logic, Handbook of Philosophical Logic 16: 115–157, 2011.
Skura, T. F., Refutations in Wansing’s logic, Reports on Mathematical Logic 52: 83–99, 2017.
Szabo, M. E., A sequent calculus for Kröger logic, in A. Salwicki, (ed.), Logics of Programs and Their Applications, Proceedings, Poznan, August 23-29, 1980, vol. 148 of Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, 1980, pp. 295–303.
Szałas, A. Concerning the semantic consequence relation in first-order temporal logic, Theoretical Computer Science 47 (3): 329–334, 1986.
Urbas, I., Dual-intuitionistic logic, Notre Dame Journal of Formal Logic 37 (3): 440–451, 1996.
Venkatesh, G., A Decision Method for Temporal Logic Based on Resolution, in S. N. Maheshwari, (ed.), Foundations of Software Technology and Theoretical Computer Science Fifth Conference, New Delhi, India, December 16-18, 1985, Proceedings, vol. 206 of Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, 1986, pp. 272–289.
Wansing, H., The Logic of Information Structures, vol. 681 of Lecture Notes in Artificial Intelligence, Springer, Berlin, Heidelberg, 1993.
Wansing, H., Semantics-based nonmonotonic inference, Notre Dame Journal of Formal Logic 36: 44–54, 1995.
Wansing, H., Falsification, natural deduction and bi-intuitionistic logic, Journal of Logic and Computation 26 (1): 425–450, 2016.
Acknowledgements
We would like to thank the anonymous referees for their valuable comments and suggestions. This research was supported by JSPS KAKENHI Grant Number JP23K10990.
Author information
Authors and Affiliations
Corresponding author
Ethics declarations
Conflict of interest
The author has no conflict of interest.
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Presented by Heinrich Wansing
Rights and permissions
Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.
About this article
Cite this article
Kamide, N. Refutation-Aware Gentzen-Style Calculi for Propositional Until-Free Linear-Time Temporal Logic. Stud Logica 111, 979–1014 (2023). https://doi.org/10.1007/s11225-023-10052-7
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11225-023-10052-7