1 Search Results for "Kimura, Daisuke"

Document
DOI: 10.4230/LIPIcs.FSCD.2021.11
Failure of Cut-Elimination in the Cyclic Proof System of Bunched Logic with Inductive Propositions

Authors: Kenji Saotome, Koji Nakazawa, and Daisuke Kimura

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

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.
Cite as

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)

Copy BibTex To Clipboard

@InProceedings{saotome_et_al:LIPIcs.FSCD.2021.11,
  author =	{Saotome, Kenji and Nakazawa, Koji and Kimura, Daisuke},
  title =	{{Failure of Cut-Elimination in the Cyclic Proof System of Bunched Logic with Inductive Propositions}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{11:1--11:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.11},
  URN =		{urn:nbn:de:0030-drops-142494},
  doi =		{10.4230/LIPIcs.FSCD.2021.11},
  annote =	{Keywords: cyclic proofs, cut-elimination, bunched logic, separation logic, linear logic}
}
  • Refine by Author
  • 1 Kimura, Daisuke
  • 1 Nakazawa, Koji
  • 1 Saotome, Kenji

  • Refine by Classification
  • 1 Theory of computation → Proof theory
  • 1 Theory of computation → Separation logic

  • Refine by Keyword
  • 1 bunched logic
  • 1 cut-elimination
  • 1 cyclic proofs
  • 1 linear logic
  • 1 separation logic

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2021

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