Loop-Type Sequent Calculi for Temporal Logic

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”.

This is a preview of subscription content, access via your institution.

References

  1. 1.

    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)

  2. 2.

    Alonderis, R., Giedra, H.: A proof-search system for the logic of likelihood. Log. J. IGPL (2019). https://doi.org/10.1093/jigpal/jzz022

  3. 3.

    Baaz, M., Leitsch, A., Zach, R.: Completeness of a first-order temporal logic with time gaps. Theor. Comput. Sci. 160, 241–270 (1996)

    MathSciNet  Article  Google Scholar 

  4. 4.

    Brünnler, K., Steiner, D.: Finitization for propositional linear time logic (Unpublished, available on the Web) (2006)

  5. 5.

    Brünnler, K., Lange, M.: Cut-free sequent systems for temporal logic. J. Log. Algebraic Program. 76(2), 216–225 (2008)

    MathSciNet  Article  Google Scholar 

  6. 6.

    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)

  7. 7.

    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)

  8. 8.

    Demri, S., Goranko, V., Lange, M.: Temporal Logics in Computer Science: Finite-State Systems. Cambridge University Press, Cambridge (2016)

    Book  Google Scholar 

  9. 9.

    Fisher, M., Dixon, C., Peim, M.: Clausal temporal resolution. ACM Trans. Comput. Log. 2(1), 12–56 (2001)

    MathSciNet  Article  Google Scholar 

  10. 10.

    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)

    MathSciNet  Article  Google Scholar 

  11. 11.

    Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge University Press, Cambridge (2012)

    MATH  Google Scholar 

  12. 12.

    Kokkinis, I., Studer, T.: Cyclic proofs for linear temporal logic. In: Concepts of Proof in Mathematics, Philosophy, and Computer Science, pp. 171–192 (2016)

  13. 13.

    Nide, N., Takata, S.: Deduction systems for BDI logic using sequent calculus. In: Proceedings of AAMAS-02, pp. 928–935 (2002)

  14. 14.

    Nishimura, H.: Sequential methods in propositional dynamic logic. Acta Inform. 12, 377–400 (1979)

    MathSciNet  Article  Google Scholar 

  15. 15.

    Paech, B.: Gentzen-systems for propositional temporal logics. Lect. Notes Comput. Sci. 385, 240–253 (1988)

    MathSciNet  Article  Google Scholar 

  16. 16.

    Pliuškevičienė, A.: Decision procedure for a fragment of dynamic logic. Lith. Math. J. Spec. Issue 41, 413–420 (2001)

    MathSciNet  MATH  Google Scholar 

  17. 17.

    Pliuškevičius, R.: On saturated calculi for linear temporal logic. Lect. Notes Comput. Sci. 711, 640–649 (1993)

    MathSciNet  Article  Google Scholar 

  18. 18.

    Pliuškevičius, R.: On saturation principle for a linear temporal logic. Lect. Notes Comput. Sci. 713, 289–300 (1993)

    MathSciNet  Article  Google Scholar 

  19. 19.

    Pliuškevičius, R.: Saturation replaces induction for a miniscoped linear tempo logic. Lect. Notes Comput. Sci. 735, 299–311 (1993)

    MathSciNet  Article  Google Scholar 

  20. 20.

    Pliuškevičius, R.: The saturation tableaux for linear miniscoped Horn-like temporal logic. J. Autom. Reason. 13, 391–407 (1994)

    Article  Google Scholar 

  21. 21.

    Pliuškevičius, R.: Saturated calculus for a Horn-like miniscoped linear temporal logic (in Russian). Notes Sci Semin. POMI 220, 123–144 (1995)

    Google Scholar 

  22. 22.

    Pliuškevičius, R.: Deduction-based decision procedure for a clausal miniscoped fragment of FTL. Lect. Notes Comput. Sci. 2083, 107–120 (2001)

    MathSciNet  Article  Google Scholar 

  23. 23.

    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)

    MATH  Google Scholar 

  24. 24.

    Schütte, K.: Proof Theory. Springer, Berlin (1977)

    Book  Google Scholar 

  25. 25.

    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

    MathSciNet  Article  MATH  Google Scholar 

  26. 26.

    Valiev, M.: On temporal logic of von Vright (in Russian). Soviet-Finland Colloquim on Logic, Moscow pp. 7–11 (1979)

  27. 27.

    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)

  28. 28.

    Wolper, P.: The tableau method for temporal logic: an overview. Logique et Analyse 28, 119–136 (1985)

    MathSciNet  MATH  Google Scholar 

Download references

Author information

Affiliations

Authors

Corresponding author

Correspondence to R. Alonderis.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and Permissions

About this article

Verify currency and authenticity via CrossMark

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

Download citation

Keywords

  • Temporal logics
  • Sequent calculi
  • Derivation loops