{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:43:48Z","timestamp":1740123828943,"version":"3.37.3"},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2023,2,16]],"date-time":"2023-02-16T00:00:00Z","timestamp":1676505600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,2,16]],"date-time":"2023-02-16T00:00:00Z","timestamp":1676505600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2023,10]]},"DOI":"10.1007\/s10472-023-09832-7","type":"journal-article","created":{"date-parts":[[2023,2,16]],"date-time":"2023-02-16T10:03:07Z","timestamp":1676541787000},"page":"651-673","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Mechanical certification of FOLID cyclic proofs"],"prefix":"10.1007","volume":"91","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1670-9474","authenticated-orcid":false,"given":"Sorin","family":"Stratulat","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,2,16]]},"reference":[{"key":"9832_CR1","unstructured":"Brotherston, J.: Sequent calculus proof systems for inductive definitions. PhD thesis, University of Edinburgh (2006)"},{"issue":"6","key":"9832_CR2","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). https:\/\/doi.org\/10.1093\/logcom\/exq052","journal-title":"J. Log. Comput."},{"key":"9832_CR3","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G Gentzen","year":"1935","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische schlie\u00dfen. I. Mathematische Zeitschrift 39, 176\u2013210 (1935). https:\/\/doi.org\/10.1007\/BF01201353","journal-title":"I. Mathematische Zeitschrift"},{"key":"9832_CR4","doi-asserted-by":"publisher","unstructured":"Brotherston, J., Gorogiannis, N., Petersen, R.L.: A generic cyclic theorem prover. In: APLAS-10 (10th Asian Symposium on Programming Languages and Systems). LNCS. https:\/\/doi.org\/10.1007\/978-3-642-35182-2_25, vol. 7705, pp 350\u2013367. Springer (2012)","DOI":"10.1007\/978-3-642-35182-2_25"},{"key":"9832_CR5","unstructured":"Michel, M.: Complementation is more difficult with automata on infinite words. Technical report CNET (1988)"},{"key":"9832_CR6","doi-asserted-by":"publisher","unstructured":"Stratulat, S.: Cyclic proofs with ordering constraints. In: Schmidt, R.A., Nalon, C. (eds.) TABLEAUX 2017 (26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods). LNAI. https:\/\/doi.org\/10.1007\/978-3-319-66902-1_19, vol. 10501, pp 311\u2013327. Springer (2017)","DOI":"10.1007\/978-3-319-66902-1_19"},{"key":"9832_CR7","doi-asserted-by":"publisher","unstructured":"Stratulat, S.: Validating back-links of FOLID cyclic pre-proofs. In: Berardi, S., Van Bakel, S. (eds.) CL&C\u201918 (Seventh International Workshop on Classical Logic and Computation). EPTCS, pp. 39\u201353. https:\/\/doi.org\/10.4204\/EPTCS.281.4 (2018)","DOI":"10.4204\/EPTCS.281.4"},{"key":"9832_CR8","doi-asserted-by":"publisher","unstructured":"Stratulat, S.: E-Cyclist: Implementation of an efficient validation of FOLID cyclic induction reasoning. In: Kutsia, T. (ed.) 9th International Symposium on Symbolic Computation in Software Science. Electronic Proceedings in Theoretical Computer Science, vol. 342, pp. 129\u2013135. https:\/\/doi.org\/10.4204\/EPTCS.342.11 (2021)","DOI":"10.4204\/EPTCS.342.11"},{"key":"9832_CR9","unstructured":"The Coq development team: The Coq Reference Manual. INRIA. INRIA. http:\/\/coq.inria.fr\/doc (2020)"},{"key":"9832_CR10","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/j.jsc.2016.07.014","volume":"80 Part 1","author":"S Stratulat","year":"2017","unstructured":"Stratulat, S.: Mechanically certifying formula-based Noetherian induction reasoning. J. Symb. Comput. 80 Part 1, 209\u2013249 (2017). https:\/\/doi.org\/10.1016\/j.jsc.2016.07.014","journal-title":"J. Symb. Comput."},{"key":"9832_CR11","doi-asserted-by":"publisher","unstructured":"Stratulat, S.: SPIKE, An automatic theorem prover \u2013 revisited. In: SYNASC 2020: Proceedings of the 22nd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing. https:\/\/doi.org\/10.1109\/SYNASC51798.2020.00025, pp 93\u201396. IEEE Computer Society (2020)","DOI":"10.1109\/SYNASC51798.2020.00025"},{"key":"9832_CR12","doi-asserted-by":"publisher","unstructured":"Berardi, S., Tatsuta, M.: Classical system of Martin-Lof\u2019s inductive definitions is not equivalent to cyclic proofs. Logical Methods in Computer Science 15(3). https:\/\/doi.org\/10.23638\/LMCS-15(3:10)2019 (2019)","DOI":"10.23638\/LMCS-15(3:10)2019"},{"key":"9832_CR13","doi-asserted-by":"publisher","unstructured":"Henaien, A., Stratulat, S.: Performing implicit induction reasoning with certifying proof environments. In: Bouhoula, A., Ida, T., Kamareddine, F. (eds.) Proceedings Fourth International Symposium on Symbolic Computation in Software Science, Gammarth, Tunisia, 15-17 December 2012. Electronic Proceedings in Theoretical Computer Science, vol. 122, pp. 97\u2013108. https:\/\/doi.org\/10.4204\/EPTCS.122.9 (2013)","DOI":"10.4204\/EPTCS.122.9"},{"key":"9832_CR14","doi-asserted-by":"publisher","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL \u201901: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. https:\/\/doi.org\/10.1145\/360204.360210, vol. 36, pp 81\u201392. ACM Press (2001)","DOI":"10.1145\/360204.360210"},{"key":"9832_CR15","doi-asserted-by":"publisher","unstructured":"Fogarty, S., Vardi, M.Y.: B\u00fcchi complementation and size-change termination. In: Kowalewski, S., Philippou, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings. Lecture Notes in Computer Science. https:\/\/doi.org\/10.1007\/978-3-642-00768-2_2, vol. 5505, pp 16\u201330. Springer (2009)","DOI":"10.1007\/978-3-642-00768-2_2"},{"key":"9832_CR16","doi-asserted-by":"publisher","unstructured":"Jones, E., Ong, C. -L., Ramsay, S.J.: Cycleq: an efficient basis for cyclic equational reasoning. In: Jhala, R., Dillig, I. (eds.) PLDI \u201922: 43Rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022, pp. 395\u2013409. ACM. https:\/\/doi.org\/10.1145\/3519939.3523731 (2022)","DOI":"10.1145\/3519939.3523731"},{"issue":"1","key":"9832_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1093\/jigpal\/12.1.1","volume":"12","author":"C-P Wirth","year":"2004","unstructured":"Wirth, C. -P.: Descente infinie + Deduction. Logic Journal of the IGPL 12(1), 1\u201396 (2004). https:\/\/doi.org\/10.1093\/jigpal\/12.1.1","journal-title":"Logic Journal of the IGPL"},{"key":"9832_CR18","doi-asserted-by":"publisher","unstructured":"Stratulat, S.: A Unified View of Induction Reasoning for First-Order Logic. In: Voronkov, A. (ed.) Turing-100 (The Alan Turing Centenary Conference). EPic Series, vol. 10, pp. 326\u2013352. Easychair. https:\/\/doi.org\/10.29007\/nsx4 (2012)","DOI":"10.29007\/nsx4"},{"key":"9832_CR19","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998). https:\/\/doi.org\/10.1017\/CBO9781139172752"},{"key":"9832_CR20","doi-asserted-by":"publisher","unstructured":"Contejean, E., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Certification of automated termination proofs. Frontiers of Combining Systems, 148\u2013162. https:\/\/doi.org\/10.1007\/978-3-540-74621-8_10 (2007)","DOI":"10.1007\/978-3-540-74621-8_10"},{"key":"9832_CR21","doi-asserted-by":"publisher","unstructured":"Contejean, E., Paskevich, A., Urbain, X., Courtieu, P., Pons, O., Forest, J.: A3PAT, an approach for certified automated termination proofs. In: Gallagher, J.P., Voigtl\u00e4nder, J. (eds.) PEPM - Proceedings of the 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2010, Madrid, Spain, pp. 63\u201372. ACM. https:\/\/doi.org\/10.1145\/1706356.1706370 (2010)","DOI":"10.1145\/1706356.1706370"},{"key":"9832_CR22","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. Springer, New York (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-023-09832-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10472-023-09832-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-023-09832-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,17]],"date-time":"2023-10-17T02:03:48Z","timestamp":1697508228000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10472-023-09832-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,2,16]]},"references-count":22,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2023,10]]}},"alternative-id":["9832"],"URL":"https:\/\/doi.org\/10.1007\/s10472-023-09832-7","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"type":"print","value":"1012-2443"},{"type":"electronic","value":"1573-7470"}],"subject":[],"published":{"date-parts":[[2023,2,16]]},"assertion":[{"value":"13 January 2023","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 February 2023","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The author declares that there are no funding and\/or conflicts of interests\/competing interests that are relevant to the content of this article.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"<!--Emphasis Type='Bold' removed-->Conflict of Interests"}}]}}