Document Open Access Logo

A Cyclic Proof System for HFL_ℕ

Authors Mayuko Kori , Takeshi Tsukada , Naoki Kobayashi

PDF
Thumbnail PDF

File

LIPIcs.CSL.2021.29.pdf
  • Filesize: 0.58 MB
  • 22 pages

Document Identifiers

Author Details

Mayuko Kori
  • Department of Informatics, The Graduate University for Advanced Studies (SOKENDAI), Hayama, Japan
  • National Institute of Informatics, Tokyo, Japan
Takeshi Tsukada
  • Graduate School of Science, Chiba University, Japan
Naoki Kobayashi
  • The University of Tokyo, Japan

Funding

This work was supported by JSPS KAKENHI Grant Number JP15H05706, JP20H00577, and JP20H05703.
  • Kori, Mayuko: The first author is supported by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST.

Acknowledgements

We would like to thank anonymous referees for useful comments.

Cite AsGet BibTex

Mayuko Kori, Takeshi Tsukada, and Naoki Kobayashi. A Cyclic Proof System for HFL_ℕ. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 29:1-29:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CSL.2021.29

Abstract

A cyclic proof system allows us to perform inductive reasoning without explicit inductions. We propose a cyclic proof system for HFL_ℕ, which is a higher-order predicate logic with natural numbers and alternating fixed-points. Ours is the first cyclic proof system for a higher-order logic, to our knowledge. Due to the presence of higher-order predicates and alternating fixed-points, our cyclic proof system requires a more delicate global condition on cyclic proofs than the original system of Brotherston and Simpson. We prove the decidability of checking the global condition and soundness of this system, and also prove a restricted form of standard completeness for an infinitary variant of our cyclic proof system. A potential application of our cyclic proof system is semi-automated verification of higher-order programs, based on Kobayashi et al.’s recent work on reductions from program verification to HFL_ℕ validity checking.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
Keywords
  • Cyclic proof
  • higher-order logic
  • fixed-point logic
  • sequent calculus

Metrics

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

Related Versions

References

  1. James Brotherston, Dino Distefano, and Rasmus Lerchedahl Petersen. Automated cyclic entailment proofs in separation logic. In Nikolaj Bjørner and Viorica Sofronie-Stokkermans, editors, Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings, volume 6803 of Lecture Notes in Computer Science, pages 131-146. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22438-6_12.
  2. James Brotherston, Nikos Gorogiannis, and Rasmus Lerchedahl Petersen. A generic cyclic theorem prover. In Ranjit Jhala and Atsushi Igarashi, editors, Programming Languages and Systems, pages 350-367, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. Google Scholar
  3. James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. Journal of Logic and Computation, 21(6):1177-1216, December 2011. Google Scholar
  4. Florian Bruse. Alternating parity Krivine automata. In Erzsébet Csuhaj-Varjú, Martin Dietzfelbinger, and Zoltán Ésik, editors, Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part I, volume 8634 of Lecture Notes in Computer Science, pages 111-122. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44522-8_10.
  5. Toby Cathcart Burn, C.-H. Luke Ong, and Steven J. Ramsay. Higher-order constrained Horn clauses for verification. PACMPL, 2(POPL):11:1-11:28, 2018. URL: https://doi.org/10.1145/3158099.
  6. Patrick Cousot and Radhia Cousot. Constructive versions of Tarski’s fixed point theorems. Pacific J. Math., 82(1):43-57, 1979. URL: https://projecteuclid.org:443/euclid.pjm/1102785059.
  7. Amina Doumane. On the infinitary proof theory of logics with fixed points. Theses, Université Sorbonne Paris Cité, June 2017. Google Scholar
  8. Naoki Kobayashi, Étienne Lozes, and Florian Bruse. On the relationship between higher-order recursion schemes and higher-order fixpoint logic. ACM SIGPLAN Notices, 52(1):246-259, 2017. Google Scholar
  9. Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, and Hiroshi Unno. Temporal verification of programs via first-order fixpoint logic. In International Static Analysis Symposium, pages 413-436. Springer, 2019. Google Scholar
  10. Naoki Kobayashi, Takeshi Tsukada, and Keiichi Watanabe. Higher-order program verification via HFL model checking. In European Symposium on Programming, pages 711-738. Springer, 2018. Google Scholar
  11. Mayuko Kori, Takeshi Tsukada, and Naoki Kobayashi. A cyclic proof system for HFL_𝐍. CoRR, 2020. A longer version. URL: http://arxiv.org/abs/2010.14891.
  12. Étienne Lozes. A type-directed negation elimination. In Ralph Matthes and Matteo Mio, editors, Proceedings Tenth International Workshop on Fixed Points in Computer Science, FICS 2015, Berlin, Germany, September 11-12, 2015, volume 191 of EPTCS, pages 132-142, 2015. URL: https://doi.org/10.4204/EPTCS.191.12.
  13. Christoph Sprenger and Mads Dam. On the structure of inductive reasoning: Circular and tree-shaped proofs in the μ-calculus. In Foundations of Software Science and Computation Structures, pages 425-440. Springer Berlin Heidelberg, 2003. Google Scholar
  14. Gadi Tellez and James Brotherston. Automatically verifying temporal properties of pointer programs with cyclic proof. J. Autom. Reasoning, 64(3):555-578, 2020. URL: https://doi.org/10.1007/s10817-019-09532-0.
  15. Takeshi Tsukada. On computability of logical approaches to branching-time property verification of programs. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’20, page 886–899, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3373718.3394766.
  16. Mahesh Viswanathan and Ramesh Viswanathan. A higher order modal fixed point logic. In International Conference on Concurrency Theory, pages 512-528. Springer, 2004. Google Scholar
  17. Keiichi Watanabe, Takeshi Tsukada, Hiroki Oshikawa, and Naoki Kobayashi. Reduction from branching-time property verification of higher-order programs to HFL validity checking. In Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2019, page 22–34, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3294032.3294077.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact