Failure of Cut-Elimination in the Cyclic Proof System of Bunched Logic with Inductive Propositions

Authors Kenji Saotome, Koji Nakazawa, Daisuke Kimura



PDF
Thumbnail PDF

File

LIPIcs.FSCD.2021.11.pdf
  • Filesize: 0.61 MB
  • 14 pages

Document Identifiers

Author Details

Kenji Saotome
  • Nagoya University, Japan
Koji Nakazawa
  • Nagoya University, Japan
Daisuke Kimura
  • Toho University, Japan

Cite As Get BibTex

Kenji Saotome, Koji Nakazawa, and Daisuke Kimura. Failure of Cut-Elimination in the Cyclic Proof System of Bunched Logic with Inductive Propositions. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 11:1-11:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.FSCD.2021.11

Abstract

Cyclic proof systems are sequent-calculus style proof systems that allow circular structures representing induction, and they are considered suitable for automated inductive reasoning. However, Kimura et al. have shown that the cyclic proof system for the symbolic heap separation logic does not satisfy the cut-elimination property, one of the most fundamental properties of proof systems. This paper proves that the cyclic proof system for the bunched logic with only nullary inductive predicates does not satisfy the cut-elimination property. It is hard to adapt the existing proof technique chasing contradictory paths in cyclic proofs since the bunched logic contains the structural rules. This paper proposes a new proof technique called proof unrolling. This technique can be adapted to the symbolic heap separation logic, and it shows that the cut-elimination fails even if we restrict the inductive predicates to nullary ones.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Separation logic
Keywords
  • cyclic proofs
  • cut-elimination
  • bunched logic
  • separation logic
  • linear logic

Metrics

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

References

  1. T. Antonopoulos, N. Gorogiannis, C. Haase, M. Kanovich, and J. Ouaknine. Foundations for decision problems in separation logic with general inductive predicates. In Proceedings of FoSSaCS 2014, volume 8412 of LNCS, pages 411-425, 2014. Google Scholar
  2. D. Baelde, A. Doumane, and A. Saurin. Infinitary proof theory: the multiplicative additive case. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 of LIPIcs, pages 42:1-42:17, 2016. Google Scholar
  3. J. Brotherston. Formalised inductive reasoning in the logic of bunched implications. In Proceedings of SAS '07, volume 4634 of LNCS, pages 87-103, 2007. Google Scholar
  4. J. Brotherston, D. Distefano, and R. L. Petersen. Automated cyclic entailment proofs in separation logic. In Proceedings of CADE-23, volume 6803 of LNAI, pages 131-146, 2011. Google Scholar
  5. J. Brotherston, N. Gorogiannis, and R. L. Petersen. A generic cyclic theorem prover. In Proceedings of APLAS 2012, volume 7705 of LNCS, pages 350-367, 2012. Google Scholar
  6. J. Brotherston and A. Simpson. Sequent calculi for induction and infinite descent. Journal of Logic and Computation, 21(6):1177-1216, 2011. Google Scholar
  7. J. Fortier and L. Santocanale. Cuts for circular proofs: semantics and cut-elimination. In Computer Science Logic 2013 (CSL 2013), volume 23 of LIPIcs, pages 248-262, 2013. Google Scholar
  8. D. Kimura, K. Nakazawa, T. Terauchi, and H. Unno. Failure of cut-elimination in cyclic proofs of separation logic. Comupter Software, 37(1):39-52, 2020. Google Scholar
  9. P. O'Hearn and D. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215-244, 1999. Google Scholar
  10. D. J. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications. Springer, 2002. Google Scholar
  11. J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings of LICS 2002, pages 55-74, 2002. Google Scholar
  12. M. Tatsuta and D. Kimura. Separation logic with monadic inductive definitions and implicit existentials. In Proceedings of APLAS 2015, volume 9458 of LNCS, pages 69-89, 2015. 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