{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:02Z","timestamp":1751660522705,"version":"3.41.0"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2020,8,11]],"date-time":"2020-08-11T00:00:00Z","timestamp":1597104000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2020,10,31]]},"abstract":"<jats:p>\n            Supporting inductive reasoning is an essential component is any framework of use in computer science. To do so, the logical framework must extend that of first-order logic. Transitive closure logic is a known extension of first-order logic that is particularly straightforward to automate. While other extensions of first-order logic with inductive definitions are\n            <jats:italic>a priori<\/jats:italic>\n            parametrized by a set of inductive definitions, the addition of a single transitive closure operator has the advantage of uniformly capturing all finitary inductive definitions. To further improve the reasoning techniques for transitive closure logic, we here present an\n            <jats:italic>infinitary<\/jats:italic>\n            proof system for it, which is an\n            <jats:italic>infinite descent<\/jats:italic>\n            \u2013style counterpart to the existing (explicit induction) proof system for the logic. We show that the infinitary system is complete for the standard semantics and subsumes the explicit system. Moreover, the uniformity of the transitive closure operator allows semantically meaningful complete restrictions to be defined using simple syntactic criteria. Consequently, the restriction to regular infinitary (i.e.,\u00a0\n            <jats:italic>cyclic<\/jats:italic>\n            ) proofs provides the basis for an effective system for automating inductive reasoning.\n          <\/jats:p>","DOI":"10.1145\/3404889","type":"journal-article","created":{"date-parts":[[2020,8,11]],"date-time":"2020-08-11T16:16:29Z","timestamp":1597162589000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Non-well-founded Proof Theory of Transitive Closure Logic"],"prefix":"10.1145","volume":"21","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4271-9078","authenticated-orcid":false,"given":"Liron","family":"Cohen","sequence":"first","affiliation":[{"name":"Ben-Gurion University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reuben N. S.","family":"Rowe","sequence":"additional","affiliation":[{"name":"Royal Holloway, University of London, Egham, TW, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,8,11]]},"reference":[{"volume-title":"Proceedings of the 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS\u201917)","year":"2017","author":"Afshari Bahareh","key":"e_1_2_1_1_1"},{"volume-title":"Thirty Five Years of Automating Mathematics","author":"Avron Arnon","key":"e_1_2_1_2_1"},{"volume-title":"Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL\u201916)","year":"2016","author":"Baelde David","key":"e_1_2_1_3_1"},{"edition":"2","volume-title":"The Logic of Time","author":"van Benthem Johan","key":"e_1_2_1_4_1"},{"volume-title":"Personal Communication (10th","year":"2018","author":"Berardi Stefano","key":"e_1_2_1_5_1"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54458-7_18"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/3329995.3330049"},{"volume-title":"Handbook of Modal Logic, Patrick Blackburn, Johan van Benthem, and Frank Wolter (Eds.). Studies in Logic and Practical Reasoning","author":"Blackburn Patrick","key":"e_1_2_1_8_1"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74061-2_6"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328453"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exq052"},{"volume-title":"Handbook of Proof Theory","author":"Buss Samuel R.","key":"e_1_2_1_12_1"},{"volume-title":"Ancestral Logic and Equivalent Systems. Master\u2019s Thesis","author":"Cohen Liron","key":"e_1_2_1_13_1"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66902-1_15"},{"volume-title":"Logic, Language, Information, and Computation, U. Kohlenbach et al. (Ed.)","series-title":"Lecture Notes in Computer Science","author":"Cohen Liron","key":"e_1_2_1_15_1"},{"volume-title":"The middle ground--ancestral logic. Synthese 196 (June 11","year":"2015","author":"Cohen Liron","key":"e_1_2_1_16_1"},{"volume-title":"Proceedings of the 27th EACSL Annual Conference on Computer Science Logic (CSL\u201918)","year":"2018","author":"Cohen Liron","key":"e_1_2_1_17_1"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90059-2"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66902-1_16"},{"volume-title":"Proceedings of the 27th EACSL Annual Conference on Computer Science Logic (CSL\u201918)","year":"2018","author":"Das Anupam","key":"e_1_2_1_21_1"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/3329995.3330010"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.2307\/2266967"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exm077"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1112\/blms\/14.4.285"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70847-4"},{"volume-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f Per","key":"e_1_2_1_28_1","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198501275.003.0010"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00171-1"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29026-9_18"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"volume-title":"Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP\u201917)","year":"1861","author":"Reuben N.","key":"e_1_2_1_32_1"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/646794.704857"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54458-7_17"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36576-1_27"},{"volume-title":"Proof Theory","author":"Takeuti Gaisi","key":"e_1_2_1_36_1"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63046-5_30"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3404889","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3404889","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:17:45Z","timestamp":1750191465000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3404889"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8,11]]},"references-count":37,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2020,10,31]]}},"alternative-id":["10.1145\/3404889"],"URL":"https:\/\/doi.org\/10.1145\/3404889","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2020,8,11]]},"assertion":[{"value":"2018-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-08-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}