{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T04:12:38Z","timestamp":1751688758634,"version":"3.41.0"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000288","name":"Royal Society","doi-asserted-by":"publisher","award":["Travel grant Cyclic Reasoning Mechanisms for Interactive Theorem Proving."],"award-info":[{"award-number":["Travel grant Cyclic Reasoning Mechanisms for Interactive Theorem Proving."]}],"id":[{"id":"10.13039\/501100000288","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>\n            Cyclic proof systems, in which induction is managed implicitly, are a promising approach to automatic verification. The soundness of cyclic proof graphs is ensured by checking them against a trace-based Infinite Descent property. Although the problem of checking Infinite Descent is known to be PSPACE-complete, this leaves much room for variation in practice. Indeed, a number of different approaches are employed across the various cyclic proof systems described in the literature. In this paper, we study criteria for Infinite Descent in an abstract, logic-independent setting. We look at criteria based on B\u00fcchi automata encodings and relational abstractions, and determine their parameterized time complexities in terms of natural dimensions of cyclic proofs: the numbers of vertices of the proof-tree graphs, and the\n            <jats:italic toggle=\"yes\">vertex width<\/jats:italic>\n            \u2014an upper bound on the number of components (e.g., formulas) of a sequent that can be simultaneously tracked for descent. We identify novel algorithms that improve upon the parameterised complexity of the existing algorithms. We implement the studied criteria and compare their performance on various benchmarks.\n          <\/jats:p>","DOI":"10.1145\/3632888","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"1352-1384","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["The Complex(ity) Landscape of Checking Infinite Descent"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6608-3000","authenticated-orcid":false,"given":"Liron","family":"Cohen","sequence":"first","affiliation":[{"name":"Ben-Gurion University of the Negev, Beersheba, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-1519-7661","authenticated-orcid":false,"given":"Adham","family":"Jabarin","sequence":"additional","affiliation":[{"name":"Ben-Gurion University of the Negev, Beersheba, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8747-0619","authenticated-orcid":false,"given":"Andrei","family":"Popescu","sequence":"additional","affiliation":[{"name":"University of Sheffield, Sheffield, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4271-9078","authenticated-orcid":false,"given":"Reuben N. S.","family":"Rowe","sequence":"additional","affiliation":[{"name":"Royal Holloway University of London, London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_14"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-15298-6_20"},{"key":"e_1_3_2_4_1","unstructured":"Dana Angluin and Dana Fisman. 2020. Polynomial Time Algorithms for Inclusion and Equivalence of Deterministic Omega Acceptors. CoRR abs\/2002.03191 (2020). arXiv:2002.03191 https:\/\/arxiv.org\/abs\/2002.03191"},{"key":"e_1_3_2_5_1","first-page":"42:1","volume-title":"25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France (LIPIcs, Vol. 62)","author":"Baelde David","year":"2016","unstructured":"David Baelde, Amina Doumane, and Alexis Saurin. 2016. Infinitary Proof Theory: the Multiplicative Additive Case. In 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France (LIPIcs, Vol. 62), Jean-Marc Talbot and Laurent Regnier (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 42:1\u201342:17. https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2016.42"},{"issue":"1","key":"e_1_3_2_6_1","first-page":"5:1","article-title":"Program Termination Analysis in Polynomial Time","volume":"29","author":"Ben-Amram Amir M.","year":"2007","unstructured":"Amir M. Ben-Amram and Chin Soon Lee. 2007. Program Termination Analysis in Polynomial Time. ACM Trans. Program. Lang. Syst. 29, 1 (2007), 5:1\u20135:37. https:\/\/doi.org\/10.1145\/1180475.1180480","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"e_1_3_2_7_1","doi-asserted-by":"crossref","unstructured":"Stefano Berardi and Makoto Tatsuta. 2017. Classical System of Martin-L\u00f6f\u2019s Inductive Definitions Is Not Equivalent to Cyclic Proof System. In Foundations of Software Science and Computation Structures - 20th International Conference FOSSACS 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software ETAPS 2017 Uppsala Sweden April 22-29 2017 Proceedings (Lecture Notes in Computer Science Vol. 10203) Javier Esparza and Andrzej S. Murawski (Eds.). 301\u2013317. https:\/\/doi.org\/10.1007\/978-3-662-54458-7_18","DOI":"10.1007\/978-3-662-54458-7_18"},{"issue":"3","key":"e_1_3_2_8_1","article-title":"Classical System of Martin-Lof\u2019s Inductive Definitions is not Equivalent to Cyclic Proofs","volume":"15","author":"Berardi Stefano","year":"2019","unstructured":"Stefano Berardi and Makoto Tatsuta. 2019. Classical System of Martin-Lof\u2019s Inductive Definitions is not Equivalent to Cyclic Proofs. Log. Methods Comput. Sci. 15, 3 (2019). https:\/\/doi.org\/10.23638\/LMCS-15(3:10)2019","journal-title":"Log. Methods Comput. Sci."},{"key":"e_1_3_2_9_1","first-page":"118","volume-title":"Language and Automata Theory and Applications, 4th International Conference, LATA 2010, Trier, Germany, May 24-28, 2010. Proceedings (Lecture Notes in Computer Science, Vol. 6031)","author":"Bousquet Nicolas","year":"2010","unstructured":"Nicolas Bousquet and Christof L\u00f6ding. 2010. Equivalence and Inclusion Problem for Strongly Unambiguous B\u00fcchi Automata. In Language and Automata Theory and Applications, 4th International Conference, LATA 2010, Trier, Germany, May 24-28, 2010. Proceedings (Lecture Notes in Computer Science, Vol. 6031), Adrian-Horia Dediu, Henning Fernau, and Carlos Mart\u00edn-Vide (Eds.). Springer, 118\u2013129. https:\/\/doi.org\/10.1007\/978-3-642-13089-2_10"},{"key":"e_1_3_2_10_1","volume-title":"Sequent Calculus Proof Systems for Inductive Definitions","author":"Brotherston James","year":"2006","unstructured":"James Brotherston. 2006. Sequent Calculus Proof Systems for Inductive Definitions. Ph.D.Dissertation. University of Edinburgh. https:\/\/era.ed.ac.uk\/handle\/1842\/1458"},{"key":"e_1_3_2_11_1","doi-asserted-by":"crossref","unstructured":"James Brotherston Richard Bornat and Cristiano Calcagno. 2008. Cyclic proofs of program termination in separation logic. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2008 San Francisco California USA January 7-12 2008 George C. Necula and Philip Wadler (Eds.). ACM 101\u2013112. https:\/\/doi.org\/10.1145\/1328438.1328453","DOI":"10.1145\/1328438.1328453"},{"key":"e_1_3_2_12_1","first-page":"68","volume-title":"Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings (Lecture Notes in Computer Science, Vol. 8723)","author":"Brotherston James","year":"2014","unstructured":"James Brotherston and Nikos Gorogiannis. 2014. Cyclic Abduction of Inductively Defined Safety and Termination Preconditions. In Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings (Lecture Notes in Computer Science, Vol. 8723), Markus M\u00fcller-Olm and Helmut Seidl (Eds.). Springer, 68\u201384. https:\/\/doi.org\/10.1007\/978-3-319-10936-7_5"},{"key":"e_1_3_2_13_1","first-page":"350","volume-title":"Programming Languages and Systems - 10th Asian Symposium, APLAS 2012, Kyoto, Japan, December 11-13, 2012. Proceedings (Lecture Notes in Computer Science, Vol. 7705)","author":"Brotherston James","year":"2012","unstructured":"James Brotherston, Nikos Gorogiannis, and Rasmus Lerchedahl Petersen. 2012. A Generic Cyclic Theorem Prover. In Programming Languages and Systems - 10th Asian Symposium, APLAS 2012, Kyoto, Japan, December 11-13, 2012. Proceedings (Lecture Notes in Computer Science, Vol. 7705), Ranjit Jhala and Atsushi Igarashi (Eds.). Springer, 350\u2013367. https: \/\/doi.org\/10.1007\/978-3-642-35182-2_25"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exq052"},{"key":"e_1_3_2_15_1","unstructured":"Khoo Siau Cheng Chin Wei Ngan Ta Quang Trung Le Ton Chanh Aishwarya Sivaraman and Nguyen Thanh Toan. 2016. Songbird Prover. https:\/\/songbird-prover.github.io\/"},{"key":"e_1_3_2_16_1","doi-asserted-by":"crossref","unstructured":"Liron Cohen Adham Jabarin Andrei Popescu and Reuben Rowe. 2023. The Complex(ity) Landscape of Checking Infinite Descent: Source Code and Evaluation Data. https:\/\/doi.org\/10.5281\/zenodo.10073582","DOI":"10.1145\/3632888"},{"issue":"4","key":"e_1_3_2_17_1","first-page":"31","article-title":"Non-Well-Founded Proof Theory of Transitive Closure Logic","volume":"21","author":"Cohen Liron","year":"2020","unstructured":"Liron Cohen and Reuben N. S. Rowe. 2020. Non-Well-Founded Proof Theory of Transitive Closure Logic. ACM Trans. Comput. Logic 21, 4, Article 31 (Aug. 2020), 31 pages. https:\/\/doi.org\/10.1145\/3404889","journal-title":"ACM Trans. Comput. Logic"},{"key":"e_1_3_2_18_1","unstructured":"The Cyclist Project Developers. 2023. The Cyclist Framework and Provers. https:\/\/github.com\/ngorogiannis\/cyclist\/ releases\/tag\/POPL2024"},{"issue":"1","key":"e_1_3_2_19_1","article-title":"The Logical Complexity of Cyclic Arithmetic","volume":"16","author":"Das Anupam","year":"2020","unstructured":"Anupam Das. 2020. On The Logical Complexity of Cyclic Arithmetic. Log. Methods Comput. Sci. 16, 1 (2020). https:\/\/doi.org\/10.23638\/LMCS-16(1:1)2020","journal-title":"Log. Methods Comput. Sci."},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-10769-6_30"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1137\/070697720"},{"key":"e_1_3_2_22_1","first-page":"273","volume-title":"FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings (Lecture Notes in Computer Science, Vol. 4337)","author":"Dax Christian","year":"2006","unstructured":"Christian Dax, Martin Hofmann, and Martin Lange. 2006. A Proof System for the Linear Time \u03bc-Calculus. In FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings (Lecture Notes in Computer Science, Vol. 4337), S. Arun-Kumar and Naveen Garg (Eds.). Springer, 273\u2013284. https:\/\/doi.org\/10.1007\/11944836_26"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","unstructured":"Amina Doumane. 2017. Constructive Completeness for the Linear-time \u03bc-calculus. In Proceedings of the 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science LICS 2017. 1\u201312. https:\/\/doi.org\/10.1109\/LICS.2017.8005075 10.1109\/LICS.2017.8005075","DOI":"10.1109\/LICS.2017.8005075"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_2"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_17"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2022.23"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454087"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523731"},{"key":"e_1_3_2_31_1","volume-title":"Tableau Systems for the Modal \u03bc-Calculus","author":"Jungteerapanich Natthapong","year":"2010","unstructured":"Natthapong Jungteerapanich. 2010. Tableau Systems for the Modal \u03bc-Calculus. Ph. D. Dissertation. University of Edingburgh. http:\/\/hdl.handle.net\/1842\/4208"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0171-7"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24364-6_3"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","unstructured":"Chin Soon Lee Neil D. Jones and Amir M. Ben-Amram. 2001. The Size-change Principle for Program Termination. In Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages London UK January 17-19 2001 Chris Hankin and Dave Schmidt (Eds.). ACM 81\u201392. https:\/\/doi.org\/10.1145\/360204.360210 10.1145\/360204.360210","DOI":"10.1145\/360204.360210"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90056-1"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3285955"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29026-9_18"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","unstructured":"Lawrence C. Paulson and Jasmin Christian Blanchette. 2010. Three years of experience with Sledgehammer a Practical Link Between Automatic and Interactive Theorem Provers. In The 8th International Workshop on the Implementation of Logics IWIL 2010 Yogyakarta Indonesia October 9 2011 (EPiC Series in Computing Vol. 2) Geoff Sutcliffe Stephan Schulz and Eugenia Ternovska (Eds.). EasyChair 1\u201311. https:\/\/doi.org\/10.29007\/36dt 10.29007\/36dt","DOI":"10.29007\/36dt"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","unstructured":"Reuben N. S. Rowe and James Brotherston. 2017. Automatic cyclic termination proofs for recursive procedures in separation logic. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs CPP 2017 Paris France January 16-17 2017 Yves Bertot and Viktor Vafeiadis (Eds.). ACM 53\u201365. https:\/\/doi.org\/10.1145\/3018610.3018623 10.1145\/3018610.3018623","DOI":"10.1145\/3018610.3018623"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45931-6_25"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.STACS.2009.1854"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.14279\/TUJ.ECEASST.76.1073"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","unstructured":"Alex Simpson. 2017. Cyclic Arithmetic Is Equivalent to Peano Arithmetic. In Foundations of Software Science and Computation Structures - 20th International Conference FOSSACS 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software ETAPS 2017 Uppsala Sweden April 22-29 2017 Proceedings (Lecture Notes in Computer Science Vol. 10203) Javier Esparza and Andrzej S. Murawski (Eds.). 283\u2013300. https:\/\/doi.org\/10.1007\/978-3-662-54458-7_17 10.1007\/978-3-662-54458-7_17","DOI":"10.1007\/978-3-662-54458-7_17"},{"key":"e_1_3_2_44_1","first-page":"22","volume-title":"Fixed Points in Computer Science, FICS 2002, Copenhagen, Denmark, 20-21 July 2002, Preliminary Proceedings (BRICS Notes Series, Vol. NS-02-2)","author":"Sprenger Christoph","year":"2002","unstructured":"Christoph Sprenger and Mads Dam. 2002. A note on global induction in a mu-calculus with explicit approximations. In Fixed Points in Computer Science, FICS 2002, Copenhagen, Denmark, 20-21 July 2002, Preliminary Proceedings (BRICS Notes Series, Vol. NS-02-2), Zolt\u00e1n \u00c9sik and Anna Ing\u00f3lfsd\u00f3ttir (Eds.). University of Aarhus, 22\u201324. https:\/\/www.brics.dk\/NS\/02\/2"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36576-1_27"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66902-1_19"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","unstructured":"Sorin Stratulat. 2018. Validating Back-links of FOLID Cyclic Pre-proofs. In Proceedings Seventh International Workshop on Classical Logic and Computation CL&C 2018 Oxford (UK) 7th of July 2018 (EPTCS Vol. 281) Stefano Berardi and Alexandre Miquel (Eds.). 39\u201353. https:\/\/doi.org\/10.4204\/EPTCS.281.4 10.4204\/EPTCS.281.4","DOI":"10.4204\/EPTCS.281.4"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","unstructured":"Sorin Stratulat. 2021. E-Cyclist: Implementation of an Efficient Validation of FOLID Cyclic Induction Reasoning. In Proceedings of the 9th International Symposium on Symbolic Computation in Software Science SCSS 2021 Hagenberg Austria September 8-10 2021 (EPTCS Vol. 342) Temur Kutsia (Ed.). 129\u2013135. https:\/\/doi.org\/10.4204\/EPTCS.342.11 10.4204\/EPTCS.342.11","DOI":"10.4204\/EPTCS.342.11"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","unstructured":"Quang-Trung Ta Ton Chanh Le Siau-Cheng Khoo and Wei-Ngan Chin. 2016. Automated Mutual Explicit Induction Proof in Separation Logic. In FM 2016: Formal Methods - 21st International Symposium Limassol Cyprus November 9-11 2016 Proceedings (Lecture Notes in Computer Science Vol. 9995) John S. Fitzgerald Constance L. Heitmeyer Stefania Gnesi and Anna Philippou (Eds.). 659\u2013676. https:\/\/doi.org\/10.1007\/978-3-319-48989-6_40 10.1007\/978-3-319-48989-6_40","DOI":"10.1007\/978-3-319-48989-6_40"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158097"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1137\/0201010"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09532-0"},{"key":"e_1_3_2_53_1","volume-title":"Representation Matters in Cyclic Proof Theory","author":"Wehr Dominik","year":"2023","unstructured":"Dominik Wehr. 2023. Representation Matters in Cyclic Proof Theory. Licentiate Thesis. University of Gothenburg. https:\/\/hdl.handle.net\/2077\/75984"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/298514.298576"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632888","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632888","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:06:14Z","timestamp":1751659574000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632888"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":53,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632888"],"URL":"https:\/\/doi.org\/10.1145\/3632888","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}