Document Open Access Logo

Cyclic Proofs for Transfinite Expressions

Authors Emile Hazard, Denis Kuperberg

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2022.23.pdf
  • Filesize: 0.79 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Proof theory
  • Theory of computation → Logic and verification
Keywords
  • transfinite expressions
  • transfinite automata
  • cyclic proofs

Metrics

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

Abstract

We introduce a cyclic proof system for proving inclusions of transfinite expressions, describing languages of words of ordinal length. We show that recognising valid cyclic proofs is decidable, that our system is sound and complete, and well-behaved with respect to cuts. Moreover, cyclic proofs can be effectively computed from expressions inclusions. We show how to use this to obtain a Pspace algorithm for transfinite expression inclusion.

Cite As Get BibTex

Emile Hazard and Denis Kuperberg. Cyclic Proofs for Transfinite Expressions. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CSL.2022.23

Author Details

Emile Hazard
  • LIP, ENS Lyon, France
Denis Kuperberg
  • CNRS, LIP, ENS Lyon, France

References

  1. Parosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukás Holík, Chih-Duo Hong, Richard Mayr, and Tomás Vojnar. Simulation subsumption in ramsey-based Büchi automata universality and inclusion testing. In CAV, volume 6174 of LNCS, pages 132-147. Springer Verlag, 2010. URL: https://doi.org/10.1007/978-3-642-14295-6_14.
  2. Bahareh Afshari and Graham E. Leigh. Cut-free completeness for modal mu-calculus. In LICS, pages 1-12. IEEE, 2017. URL: https://doi.org/10.1109/LICS.2017.8005088.
  3. Nicolas Bedon. Finite automata and ordinals. Theor. Comput. Sci., 156(1&2):119-144, 1996. URL: https://doi.org/10.1016/0304-3975(95)00006-2.
  4. Filippo Bonchi and Damien Pous. Checking NFA equivalence with bisimulations up to congruence. In POPL, pages 457-468. ACM, 2013. URL: https://doi.org/10.1145/2429069.2429124.
  5. James Brotherston. Cyclic proofs for first-order logic with inductive definitions. In TABLEAUX, volume 3702 of Lecture Notes in Artificial Intelligence, pages 78-92. Springer Verlag, 2005. URL: https://doi.org/10.1007/11554554_8.
  6. James Brotherston and Alex Simpson. Complete sequent calculi for induction and infinite descent. In 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pages 51-62, 2007. URL: https://doi.org/10.1109/LICS.2007.16.
  7. Samuel Buss. The undecidability of k-provability. Annals of Pure and Applied Logic, 53(1):75-102, 1991. URL: https://doi.org/10.1016/0168-0072(91)90059-U.
  8. Yaacov Choueka. Finite automata, definable sets, and regular expressions over ωⁿ-tapes. J. Comput. Syst. Sci., 17(1):81-97, 1978. URL: https://doi.org/10.1016/0022-0000(78)90036-3.
  9. Liron Cohen and Reuben N. S. Rowe. Integrating induction and coinduction via closure operators and proof cycles. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning, pages 375-394, Cham, 2020. Springer International Publishing. Google Scholar
  10. James Cranch, Michael R. Laurence, and Georg Struth. Completeness results for omega-regular algebras. J. Log. Algebr. Meth. Program., 84(3):402-425, 2015. URL: https://doi.org/10.1016/j.jlamp.2014.10.002.
  11. Anupam Das and Damien Pous. A cut-free cyclic proof system for kleene algebra. In Renate A. Schmidt and Cláudia Nalon, editors, Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25-28, 2017, Proceedings, volume 10501 of Lecture Notes in Computer Science, pages 261-277. Springer, 2017. Google Scholar
  12. Anupam Das and Damien Pous. Non-wellfounded proof theory for (Kleene+Action)(Algebras+Lattices). In 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK, pages 19:1-19:18, 2018. Google Scholar
  13. Christian Dax, Martin Hofmann, and Martin Lange. A proof system for the linear time μ-calculus. In S. Arun-Kumar and Naveen Garg, editors, FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, pages 273-284, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  14. Stephane Demri and Alexander Rabinovich. The complexity of linear-time temporal logic over the class of ordinals. Logical Methods in Computer Science, 6, September 2010. URL: https://doi.org/10.2168/LMCS-6(4:9)2010.
  15. Amina Doumane, David Baelde, Lucca Hirschi, and Alexis Saurin. Towards completeness via proof search in the linear time μ-calculus: The case of büchi inclusions. In LICS, pages 377-386. ACM, 2016. URL: https://doi.org/10.1145/2933575.2933598.
  16. Ioannis Kokkinis and Thomas Studer. Cyclic proofs for linear temporal logic. Concepts of Proof in Mathematics, Philosophy, and Computer Science, 6:171, 2016. Google Scholar
  17. D. Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation, 110(2):366-390, 1994. URL: https://doi.org/10.1006/inco.1994.1037.
  18. Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. The size-change principle for program termination. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '01, pages 81-92, New York, NY, USA, 2001. Association for Computing Machinery. URL: https://doi.org/10.1145/360204.360210.
  19. S. Safra. On the complexity of omega -automata. In [Proceedings 1988] 29th Annual Symposium on Foundations of Computer Science, pages 319-327, 1988. URL: https://doi.org/10.1109/SFCS.1988.21948.
  20. Alex Simpson. Cyclic arithmetic is equivalent to peano arithmetic. In FoSSaCS, volume 10203 of Lecture Notes in Computer Science, pages 283-300. Springer Verlag, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_17.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact