{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,6]],"date-time":"2026-04-06T05:20:45Z","timestamp":1775452845100,"version":"3.50.1"},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T00:00:00Z","timestamp":1763683200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T00:00:00Z","timestamp":1763683200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["22K11901"],"award-info":[{"award-number":["22K11901"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Arch. Math. Logic"],"published-print":{"date-parts":[[2026,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Cyclic-proof systems are sequent-calculus-style proof systems that allow circular structures that represent induction. Cyclic-proof systems are considered suitable for automated inductive reasoning, and the cut-elimination property is desirable because finding cut formulas often requires heuristics. However, the cut-elimination property does not hold in some cyclic-proof systems, such as the sequent calculus for first-order logic and the entailment system for symbolic-heap separation logic. This paper proves that the cyclic-proof system for the logic of bunched implications does not satisfy the cut-elimination property, even if the system is restricted to the positive fragment with inductively defined propositions. To prove this, we use a new proof technique called proof unrolling. To demonstrate that proof unrolling is a general technique, this paper adapts proof unrolling to another cyclic-proof system for multiplicative additive linear logic with fixed-point operators.<\/jats:p>","DOI":"10.1007\/s00153-025-00993-2","type":"journal-article","created":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T19:39:16Z","timestamp":1763753956000},"page":"333-362","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Failure of cut-elimination in cyclic-proof systems of logic of bunched implications with inductive propositions"],"prefix":"10.1007","volume":"65","author":[{"given":"Kenji","family":"Saotome","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Koji","family":"Nakazawa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daisuke","family":"Kimura","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ayumu","family":"Kawasaki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,21]]},"reference":[{"key":"993_CR1","unstructured":"Doumane, A.: On the infinitary proof theory of logics with fixed points. PhD thesis, Paris\u00a07 (2017)"},{"key":"993_CR2","doi-asserted-by":"crossref","unstructured":"Brotherston, J.: Formalised inductive reasoning in the logic of bunched implications. In: Proceedings of SAS \u201907. LNCS, vol. 4634, pp. 87\u2013103 (2007)","DOI":"10.1007\/978-3-540-74061-2_6"},{"key":"993_CR3","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Distefano, D., Petersen, R.L.: Automated cyclic entailment proofs in separation logic. In: Proceedings of CADE-23. LNAI, vol. 6803, pp. 131\u2013146 (2011)","DOI":"10.1007\/978-3-642-22438-6_12"},{"key":"993_CR4","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Gorogiannis, N., Petersen, R.L.: A generic cyclic theorem prover. In: Proceedings of APLAS 2012. LNCS, vol. 7705, pp. 350\u2013367 (2012)","DOI":"10.1007\/978-3-642-35182-2_25"},{"key":"993_CR5","doi-asserted-by":"crossref","unstructured":"Chu, D., Jaffar, J., Trinh, M.: Automatic induction proofs of data-structures in imperative programs. In: Proceedings of PLDI 2015, pp. 457\u2013466 (2015)","DOI":"10.1145\/2737924.2737984"},{"key":"993_CR6","doi-asserted-by":"crossref","unstructured":"Ta, Q., Le, T.C., Khoo, S., Chin, W.: Automated mutual induction in separation logic. In: Proceedings of FM 2016. LNCS, vol. 9995, pp. 659\u2013676 (2016)","DOI":"10.1007\/978-3-319-48989-6_40"},{"key":"993_CR7","doi-asserted-by":"crossref","unstructured":"Tatsuta, M., Nakazawa, K., Kimura, D.: Completeness of cyclic proofs for symbolic heaps with inductive definitions. In: Proceedings of APLAS 2019. LNCS, vol. 11893, pp. 367\u2013387 (2019)","DOI":"10.1007\/978-3-030-34175-6_19"},{"issue":"2","key":"993_CR8","doi-asserted-by":"publisher","first-page":"215","DOI":"10.2307\/421090","volume":"5","author":"PW O\u2019Hearn","year":"1999","unstructured":"O\u2019Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bull. Symb. Log. 5(2), 215\u2013244 (1999)","journal-title":"Bull. Symb. Log."},{"key":"993_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-0091-7","volume-title":"The Semantics and Proof Theory of the Logic of Bunched Implications","author":"DJ Pym","year":"2002","unstructured":"Pym, D.J.: The Semantics and Proof Theory of the Logic of Bunched Implications. Springer, Dordrecht (2002)"},{"issue":"6","key":"993_CR10","doi-asserted-by":"publisher","first-page":"1177","DOI":"10.1093\/logcom\/exq052","volume":"21","author":"J Brotherston","year":"2011","unstructured":"Brotherston, J., Simpson, A.: Sequent calculi for induction and infinite descent. J. Log. Comput. 21(6), 1177\u20131216 (2011)","journal-title":"J. Log. Comput."},{"key":"993_CR11","unstructured":"Fortier, J., Santocanale, L.: Cuts for circular proofs: semantics and cut-elimination. In: Computer Science Logic 2013 (CSL 2013). LIPIcs, vol. 23, pp. 248\u2013262 (2013)"},{"key":"993_CR12","unstructured":"Baelde, D., Doumane, A., Saurin, A.: Infinitary proof theory: the multiplicative additive case. In: 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). LIPIcs, vol. 62, pp. 42\u201314217 (2016)"},{"key":"993_CR13","doi-asserted-by":"publisher","unstructured":"Masuoka, Y., Tatsuta, M.: Counterexample to cut-elimination in cyclic proof system for first-order logic with inductive definitions. Available at https:\/\/doi.org\/10.48550\/arXiv.2106.11798 (2021)","DOI":"10.48550\/arXiv.2106.11798"},{"issue":"1","key":"993_CR14","first-page":"39","volume":"37","author":"D Kimura","year":"2020","unstructured":"Kimura, D., Nakazawa, K., Terauchi, T., Unno, H.: Failure of cut-elimination in cyclic proofs of separation logic. Comupter Software 37(1), 39\u201352 (2020)","journal-title":"Comupter Software"},{"key":"993_CR15","unstructured":"Kimura, D., Nakazawa, K., Saotome, K.: Cut-elimination for cyclic proof systems with inductively defined propositions. In: Theory and Applications of Proof and Computation. RIMS Kokyuroku, vol. 2228, pp. 59\u201372 (2022)"},{"key":"993_CR16","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proceedings of LICS 2002, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"993_CR17","doi-asserted-by":"crossref","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: A decidable fragment of separation logic. In: Proceedings of FSTTCS 2004. LNCS, vol. 3328, pp. 97\u2013109 (2004)","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"993_CR18","unstructured":"Saotome, K., Nakazawa, K., Kimura, D.: Failure of cut-elimination in cyclic proofs of bunched logic with inductive propositions. In: 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol. 195, pp. 11\u201311114 (2021)"},{"key":"993_CR19","unstructured":"Das, A., De, A., Saurin, A.: Decision problems for linear logic with least and greatest fixed points. In: 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 228, pp. 20\u201312020 (2022)"}],"container-title":["Archive for Mathematical Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-025-00993-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00153-025-00993-2","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-025-00993-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,6]],"date-time":"2026-04-06T03:59:18Z","timestamp":1775447958000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00153-025-00993-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,21]]},"references-count":19,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2026,3]]}},"alternative-id":["993"],"URL":"https:\/\/doi.org\/10.1007\/s00153-025-00993-2","relation":{},"ISSN":["0933-5846","1432-0665"],"issn-type":[{"value":"0933-5846","type":"print"},{"value":"1432-0665","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,21]]},"assertion":[{"value":"29 January 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 October 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 November 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have no relevant financial or non-financial interests to disclose.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflicts of interest\/Competing interests"}}]}}