Abstract
Various types of calculi (Hilbert, Gentzen sequent, resolution calculi, tableaux) for propositional linear temporal logic (PLTL) have been invented. In this paper, a sound and complete loop-type sequent calculus \(\mathbf{G} _\text {L}{} \mathbf{T} \) for PLTL with the temporal operators “next” and “henceforth always” (\({\mathbf{PLTL}}^{n,a}\)) is considered at first. We prove that all rules of \(\mathbf{G} _\text {L}{} \mathbf{T} \) are invertible and that the structural rules of weakening and contraction, as well as the rule of cut, are admissible in \(\mathbf{G} _\text {L}{} \mathbf{T} \). We describe a decision procedure for \({\mathbf{PLTL}}^{n,a}\) based on the introduced calculus \(\mathbf{G} _\text {L}{} \mathbf{T} \). Afterwards, we introduce a sound and complete sequent calculus \(\mathbf{G} _\text {L}{} \mathbf{T} ^\mathcal {U}\) for PLTL with the temporal operators “next” and “until”.
Similar content being viewed by others
References
Afshari, B., Leigh, G.E.: Cut-free completeness for modal mu-calculus. In: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Reykjavik, Iceland, 1–12 (2017)
Alonderis, R., Giedra, H.: A proof-search system for the logic of likelihood. Log. J. IGPL (2019). https://doi.org/10.1093/jigpal/jzz022
Baaz, M., Leitsch, A., Zach, R.: Completeness of a first-order temporal logic with time gaps. Theor. Comput. Sci. 160, 241–270 (1996)
Brünnler, K., Steiner, D.: Finitization for propositional linear time logic (Unpublished, available on the Web) (2006)
Brünnler, K., Lange, M.: Cut-free sequent systems for temporal logic. J. Log. Algebraic Program. 76(2), 216–225 (2008)
Cranen, S., Groote, J., Reniers, M.: A linear translation from LTL to the first-order modal \(\mu \)-calculus. Technical Report 10-09, Computer Science Reports (2010)
Dax C., Hofmann M., Lange M.: A proof system for the linear time \(\mu \)-calculus. In: Arun-Kumar, S., Garg, N. (eds) FSTTCS 2006 (2006)
Demri, S., Goranko, V., Lange, M.: Temporal Logics in Computer Science: Finite-State Systems. Cambridge University Press, Cambridge (2016)
Fisher, M., Dixon, C., Peim, M.: Clausal temporal resolution. ACM Trans. Comput. Log. 2(1), 12–56 (2001)
Gaintzarain, J., Hermo, M., Lucio, P., Navarro, M., Orejas, F.: A cut-free and invariant-free sequent calculus for PLTL. Lect. Notes Comput. Sci. 4646, 481–495 (2007)
Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge University Press, Cambridge (2012)
Kokkinis, I., Studer, T.: Cyclic proofs for linear temporal logic. In: Concepts of Proof in Mathematics, Philosophy, and Computer Science, pp. 171–192 (2016)
Nide, N., Takata, S.: Deduction systems for BDI logic using sequent calculus. In: Proceedings of AAMAS-02, pp. 928–935 (2002)
Nishimura, H.: Sequential methods in propositional dynamic logic. Acta Inform. 12, 377–400 (1979)
Paech, B.: Gentzen-systems for propositional temporal logics. Lect. Notes Comput. Sci. 385, 240–253 (1988)
Pliuškevičienė, A.: Decision procedure for a fragment of dynamic logic. Lith. Math. J. Spec. Issue 41, 413–420 (2001)
Pliuškevičius, R.: On saturated calculi for linear temporal logic. Lect. Notes Comput. Sci. 711, 640–649 (1993)
Pliuškevičius, R.: On saturation principle for a linear temporal logic. Lect. Notes Comput. Sci. 713, 289–300 (1993)
Pliuškevičius, R.: Saturation replaces induction for a miniscoped linear tempo logic. Lect. Notes Comput. Sci. 735, 299–311 (1993)
Pliuškevičius, R.: The saturation tableaux for linear miniscoped Horn-like temporal logic. J. Autom. Reason. 13, 391–407 (1994)
Pliuškevičius, R.: Saturated calculus for a Horn-like miniscoped linear temporal logic (in Russian). Notes Sci Semin. POMI 220, 123–144 (1995)
Pliuškevičius, R.: Deduction-based decision procedure for a clausal miniscoped fragment of FTL. Lect. Notes Comput. Sci. 2083, 107–120 (2001)
Pliuškevičius, R., Pliuškevičienė, A.: Decision procedure for a fragment of mutual belief logic with quantified agent variables. Lect. Notes Artif. Intell. 3900, 112–128 (2006)
Schütte, K.: Proof Theory. Springer, Berlin (1977)
Sundholm, G.: A completeness proof for an infinitary tense-logic. Theoria 43, 47–51 (1977). https://doi.org/10.1111/j.1755-2567.1977.tb00778.x
Valiev, M.: On temporal logic of von Vright (in Russian). Soviet-Finland Colloquim on Logic, Moscow pp. 7–11 (1979)
Valiev, M.K.: Decision complexity of variants of propositional dynamic logic. In: Dembinski, P. (ed) Proceedings of MFCS’80LNCS 88, pp. 656–664. Springer, Berlin (1980)
Wolper, P.: The tableau method for temporal logic: an overview. Logique et Analyse 28, 119–136 (1985)
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
About this article
Cite this article
Alonderis, R., Pliuškevičius, R., Pliuškevičienė, A. et al. Loop-Type Sequent Calculi for Temporal Logic. J Autom Reasoning 64, 1663–1684 (2020). https://doi.org/10.1007/s10817-020-09544-1
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-020-09544-1