Document Open Access Logo

A Hypersequent Calculus with Clusters for Tense Logic over Ordinals

Authors David Baelde, Anthony Lick, Sylvain Schmitz

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2018.15.pdf
  • Filesize: 0.57 MB
  • 19 pages

Document Identifiers

Author Details

David Baelde
  • LSV, ENS Paris-Saclay & CNRS & Inria, Université Paris-Saclay, France
Anthony Lick
  • LSV, CNRS & ENS Paris-Saclay, Université Paris-Saclay, France
Sylvain Schmitz
  • LSV, ENS Paris-Saclay & CNRS, Université Paris-Saclay, France

Funding

ANR-14-CE28-0005 prodaq

Cite AsGet BibTex

David Baelde, Anthony Lick, and Sylvain Schmitz. A Hypersequent Calculus with Clusters for Tense Logic over Ordinals. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 15:1-15:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.FSTTCS.2018.15

Abstract

Prior's tense logic forms the core of linear temporal logic, with both past- and future-looking modalities. We present a sound and complete proof system for tense logic over ordinals. Technically, this is a hypersequent system, enriched with an ordering, clusters, and annotations. The system is designed with proof search algorithms in mind, and yields an optimal coNP complexity for the validity problem. It entails a small model property for tense logic over ordinals: every satisfiable formula has a model of order type at most omega^2. It also allows to answer the validity problem for ordinals below or exactly equal to a given one.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Modal and temporal logics
Keywords
  • modal logic
  • proof system
  • hypersequent

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Arnon Avron. On Modal Systems Having Arithmetical Interpretations. Journal of Symbolic Logic, 49(3):935-942, 1984. URL: http://dx.doi.org/10.2307/2274147.
  2. Arnon Avron. Hypersequents, logical consequence and intermediate logics for concurrency. Annals of Mathematics and Artificial Intelligence, 4(3-4):225-248, 1991. URL: http://dx.doi.org/10.1007/BF01531058.
  3. David Baelde, Anthony Lick, and Sylvain Schmitz. A Hypersequent Calculus with Clusters for Linear Frames. In Proc. AiML 2018, volume 12 of Advances in Modal Logic, pages 36-55. College Publications, 2018. To appear. URL: https://hal.inria.fr/hal-01756126.
  4. David Baelde, Simon Lunel, and Sylvain Schmitz. A Sequent Calculus for a Modal Logic on Finite Data Trees. In Proc. CSL 2016, volume 62 of Leibniz International Proceedings in Informatics, pages 32:1-32:16. LZI, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2016.32.
  5. Nuel D. Belnap. Display logic. Journal of Philosophical Logic, 11(4):375-417, 1982. Google Scholar
  6. Patrick Blackburn, Marteen de Rijke, and Yde Venema. Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001. Google Scholar
  7. Kai Brünnler. Deep sequent systems for modal logic. Archiv für Mathematische Logik und Grundlagenforschung, 48(6):551-577, 2009. URL: http://dx.doi.org/10.1007/s00153-009-0137-3.
  8. Véronique Bruyère and Olivier Carton. Automata on Linear Orderings. J. Comput. Syst. Sci., 73(1):1-24, February 2007. URL: http://dx.doi.org/10.1016/j.jcss.2006.10.009.
  9. Nino B. Cocchiarella. Tense and Modal Logic: a Study in the Topology of Temporal Reference. PhD thesis, University of California, Los Angeles, 1965. Google Scholar
  10. Julien Cristau. Automata and temporal logic over arbitrary linear time. In Proc. FSTTCS 2009, volume 4 of Leibniz International Proceedings in Informatics, pages 133-144. LZI, 2009. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2009.2313.
  11. Anupam Das and Damien Pous. A Cut-Free Cyclic Proof System for Kleene Algebra. In Proc. Tableaux 2017, volume 10501 of Lecture Notes in Computer Science, pages 261-277. Springer, 2017. URL: http://dx.doi.org/10.1007/978-3-319-66902-1_16.
  12. Stephane Demri and Alexander Rabinovich. The complexity of linear-time temporal logic over the class of ordinals. Logical Methods in Computer Science, 6(4), 2010. URL: http://dx.doi.org/10.2168/LMCS-6(4:9)2010.
  13. Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. First-Order Logic with Two Variables and Unary Temporal Logic. Information and Computation, 179(2):279-295, 2002. URL: http://dx.doi.org/10.1006/inco.2001.2953.
  14. Andrzej Indrzejczak. Cut-free hypersequent calculus for S4.3. Bulletin of the Section of Logic, 41(1/2):89-104, 2012. Google Scholar
  15. Andrzej Indrzejczak. Linear Time in Hypersequent Framework. Bulletin of Symbolic Logic, 22(1):121-144, 2016. URL: http://dx.doi.org/10.1017/bsl.2016.2.
  16. Andrzej Indrzejczak. Cut Elimination Theorem for Non-Commutative Hypersequent Calculus. Bulletin of the Section of Logic, 46(1/2):135-149, 2017. URL: http://dx.doi.org/10.18778/0138-0680.46.1.2.10.
  17. Max Kanovich. The multiplicative fragment of linear logic is \NP-complete. Technical Report X-91-13, Institute for Language, Logic, and Information, 1991. Google Scholar
  18. Ryo Kashima. Cut-free sequent calculi for some tense logics. Studia Logica, 53(1):119-135, 1994. URL: http://dx.doi.org/10.1007/BF01053026.
  19. Marcus Kracht. Power and weakness of the modal display calculus. In Proof Theory of Modal Logic, pages 93-121. Springer, 1996. Google Scholar
  20. Hidenori Kurokawa. Hypersequent Calculi for Modal Logics Extending S4. In JSAI-isAI 2013, volume 8417 of Lecture Notes in Computer Science, pages 51-68. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-10061-6_4.
  21. François Laroussinie, Nicolas Markey, and Philippe Schnoebelen. Temporal logic with forgettable past. In Proc. LICS 2002, 2002. URL: http://dx.doi.org/10.1109/LICS.2002.1029846.
  22. Björn Lellmann. Linear Nested Sequents, 2-Sequents and Hypersequents. In Proc. Tableaux 2015, volume 9323 of Lecture Notes in Computer Science, pages 135-150. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-24312-2_10.
  23. Orna Lichtenstein, Amir Pnueli, and Lenore D. Zuck. The glory of the past. In Proc. Workshop on Logics of Programs, volume 193 of Lecture Notes in Computer Science, pages 196-218. Springer, 1985. URL: http://dx.doi.org/10.1007/3-540-15648-8_16.
  24. Patrick Lincoln, John Mitchell, Andre Scedrov, and Natarajan Shankar. Decision problems for propositional linear logic. Annals of Pure and Applied Logic, 56(1-3):239-311, 1992. URL: http://dx.doi.org/10.1016/0168-0072(92)90075-B.
  25. Sara Negri. Proof Analysis in Modal Logic. Journal of Philosophical Logic, 34(5):507-544, 2005. URL: http://dx.doi.org/10.1007/s10992-005-2267-3.
  26. Hiroakira Ono and Akira Nakamura. On the size of refutation Kripke models for some linear modal and tense logics. Studia Logica, 39(4):325-333, 1980. URL: http://dx.doi.org/10.1007/BF00713542.
  27. Martin Otto. Two Variable First-Order Logic Over Ordered Domains. Journal of Symbolic Logic, 66(2):685-702, 2001. URL: http://dx.doi.org/10.2307/2695037.
  28. Amir Pnueli. The temporal logic of programs. In FOCS 1977, pages 46-57. IEEE, 1977. URL: http://dx.doi.org/10.1109/SFCS.1977.32.
  29. Francesca Poggiolesi. A purely syntactic and cut-free sequent calculus for the modal logic of provability. The Review of Symbolic Logic, 2(4):593-611, 2009. URL: http://dx.doi.org/10.1017/S1755020309990244.
  30. Francesca Poggiolesi. The Method of Tree-Hypersequents for Modal Propositional Logic. In Proc. Trends in Logic IV, volume 28 of Trends in Logic, pages 31-51. Springer, 2009. URL: http://dx.doi.org/10.1007/978-1-4020-9084-4_3.
  31. Arthur N. Prior. Time and Modality. Oxford University Press, 1957. Google Scholar
  32. Alexander Rabinovich. Temporal logics over linear time domains are in \PSPACE. Information and Computation, 210:40-67, 2012. URL: http://dx.doi.org/10.1016/j.ic.2011.11.002.
  33. Gareth S. Rohde. Alternating Automata and the Temporal Logic of Ordinals. PhD thesis, University of Illinois at Urbana-Champaign, 1997. Google Scholar
  34. A. Prasad Sistla and Edmund M. Clarke. The Complexity of Propositional Linear Temporal Logics. J. ACM, 32(3):733-749, 1985. URL: http://dx.doi.org/10.1145/3828.3837.
  35. A. Prasad Sistla and Lenore D. Zuck. Reasoning in a Restricted Temporal Logic. Information and Computation, 102(2):167-195, 1993. URL: http://dx.doi.org/10.1006/inco.1993.1006.
  36. Moshe Y Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification. In LICS 1986, pages 322-331. IEEE, 1986. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact