{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T02:13:31Z","timestamp":1783649611512,"version":"3.55.0"},"reference-count":39,"publisher":"SAGE Publications","issue":"4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AIC"],"published-print":{"date-parts":[[2024,9,18]]},"abstract":"<jats:p>The CADE ATP System Competition (CASC) is the annual evaluation of fully automatic, classical logic, Automated Theorem Proving (ATP) systems\u00a0\u2013 the world championship for such systems. CASC-29 was the twenty-eighth competition in the CASC series. Twenty-four ATP systems competed in the various divisions. This paper presents an outline of the competition design and a commentated summary of the results.<\/jats:p>","DOI":"10.3233\/aic-230325","type":"journal-article","created":{"date-parts":[[2024,3,26]],"date-time":"2024-03-26T11:56:51Z","timestamp":1711454211000},"page":"485-503","source":"Crossref","is-referenced-by-count":5,"title":["The CADE-29 Automated Theorem Proving System Competition\u00a0\u2013 CASC-29"],"prefix":"10.1177","volume":"37","author":[{"given":"Geoff","family":"Sutcliffe","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Miami, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martin","family":"Desharnais","sequence":"additional","affiliation":[{"name":"Automation of Logic, Max Planck Institute for Informatics, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"179","reference":[{"key":"10.3233\/AIC-230325_ref1","doi-asserted-by":"crossref","unstructured":"A.\u00a0Bhayat, M.\u00a0Rawson and J.\u00a0Schoisswohl, Superposition with delayed unification, in: Proceedings of the 29th International Conference on Automated Deduction, B.\u00a0Pientka and C.\u00a0Tinelli, eds, Lecture Notes in Computer Science, Springer-Verlag, 2023, pp.\u00a023\u201340.","DOI":"10.1007\/978-3-031-38499-8_2"},{"key":"10.3233\/AIC-230325_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51074-9_16"},{"key":"10.3233\/AIC-230325_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-20615-8_1"},{"key":"10.3233\/AIC-230325_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_11"},{"key":"10.3233\/AIC-230325_ref5","unstructured":"F.\u00a0Bobot, M.\u00a0Bromberger and J.\u00a0Hoenicke, 18th International Satisfiability Modulo Theories Competition (SMT-COMP 2023): Rules and Procedures, 2023, https:\/\/smt-comp.github.io\/2023\/rules.pdf."},{"issue":"6","key":"10.3233\/AIC-230325_ref6","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/s10009-014-0314-5","article-title":"Let\u2019s verify this with Why3","volume":"17","author":"Bobot","year":"2015","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"10.3233\/AIC-230325_ref7","unstructured":"K.\u00a0Claessen and N.\u00a0S\u00f6rensson, New techniques that improve MACE-style finite model finding, in: Proceedings of the CADE-19 Workshop: Model Computation\u00a0\u2013 Principles, Algorithms, Applications, P.\u00a0Baumgartner and C.\u00a0Fermueller, eds, 2003."},{"key":"10.3233\/AIC-230325_ref8","doi-asserted-by":"crossref","unstructured":"L.\u00a0de\u00a0Moura and S.\u00a0Ullrich, The Lean 4 theorem prover and programming language, in: Proceedings of the 28th International Conference on Automated Deduction, A.\u00a0Platzer and G.\u00a0Sutcliffe, eds, Lecture Notes in Computer Science, Springer-Verlag, 2015, pp.\u00a0625\u2013635.","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"10.3233\/AIC-230325_ref9","unstructured":"M.\u00a0Desharnais, P.\u00a0Vukmirovi\u0107, J.\u00a0Blanchette and M.\u00a0Wnezel, Seventeen provers under the Hammer, in: Proceedings of the 13th International Conference on Interactive Theorem Proving, J.\u00a0Andronick and L.\u00a0de\u00a0Moura, eds, Leibniz International Proceedings in Informatics, Schloss Dagstuhl\u00a0\u2013 Leibniz-Zentrum f\u00fcr Informatik, 2022, pp.\u00a08:1\u20138:18."},{"key":"10.3233\/AIC-230325_ref10","doi-asserted-by":"crossref","unstructured":"H.\u00a0Ganzinger, C.\u00a0Meyer and C.\u00a0Weidenbach, Soft typing for ordered resolution, in: Proceedings of the 14th International Conference on Automated Deduction, W.W.\u00a0McCune, ed., Lecture Notes in Artificial Intelligence, Springer-Verlag, 1997, pp.\u00a0321\u2013335.","DOI":"10.1007\/3-540-63104-6_32"},{"key":"10.3233\/AIC-230325_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51074-9_23"},{"key":"10.3233\/AIC-230325_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_22"},{"key":"10.3233\/AIC-230325_ref13","doi-asserted-by":"crossref","unstructured":"J.\u00a0Jakubuv and J.\u00a0Urban, ENIGMA: Efficient learning-based inference guiding machine, in: Proceedings of the 10th International Conference on Intelligent Computer Mathematics, H.\u00a0Geuvers, M.\u00a0England, O.\u00a0Hasan, F.\u00a0Rabe and O.\u00a0Teschke, eds, Lecture Notes in Artificial Intelligence, Springer-Verlag, 2017, pp.\u00a0292\u2013302.","DOI":"10.1007\/978-3-319-62075-6_20"},{"key":"10.3233\/AIC-230325_ref15","doi-asserted-by":"crossref","unstructured":"L.\u00a0Kovacs and A.\u00a0Voronkov, First-order theorem proving and vampire, in: Proceedings of the 25th International Conference on Computer Aided Verification, N.\u00a0Sharygina and H.\u00a0Veith, eds, Lecture Notes in Artificial Intelligence, Springer-Verlag, 2013, pp.\u00a01\u201335.","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"10.3233\/AIC-230325_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52885-7_100"},{"key":"10.3233\/AIC-230325_ref17","doi-asserted-by":"publisher","DOI":"10.32473\/flairs.36.133073"},{"key":"10.3233\/AIC-230325_ref18","doi-asserted-by":"crossref","unstructured":"J.\u00a0Parsert, C.\u00a0Brown, M.\u00a0Janota and C.\u00a0Kaliszyk, Experiments on infinite model finding in SMT solving, in: Proceedings of 24th International Conference on Logic for Programming Artificial Intelligence and Reasoning, R.\u00a0Piskac and A.\u00a0Voronkov, eds, EPiC Series in Computing, EasyChair Publications, 2023, pp.\u00a0317\u2013328.","DOI":"10.29007\/slrm"},{"key":"10.3233\/AIC-230325_ref19","doi-asserted-by":"crossref","unstructured":"L.\u00a0Paulson and J.\u00a0Blanchette, Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers, in: Proceedings of the 8th International Workshop on the Implementation of Logics, G.\u00a0Sutcliffe, E.\u00a0Ternovska and S.\u00a0Schulz, eds, EPiC Series in Computing, EasyChair Publications, 2010, pp.\u00a01\u201311.","DOI":"10.29007\/36dt"},{"issue":"2\u20133","key":"10.3233\/AIC-230325_ref20","first-page":"79","article-title":"The development of CASC","volume":"15","author":"Pelletier","year":"2002","journal-title":"AI Communications"},{"issue":"1\u20132","key":"10.3233\/AIC-230325_ref21","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0747-7171(03)00040-3","article-title":"Limited resource strategy in resolution theorem proving","volume":"36","author":"Riazanov","year":"2003","journal-title":"Journal of Symbolic Computation"},{"key":"10.3233\/AIC-230325_ref22","unstructured":"A.\u00a0Robinson and A.\u00a0Voronkov, Handbook of Automated Reasoning, Elsevier Science, 2001."},{"issue":"4","key":"10.3233\/AIC-230325_ref23","doi-asserted-by":"publisher","first-page":"139","DOI":"10.3233\/SAT190083","article-title":"Controlling a solver execution with the runsolver tool","volume":"7","author":"Roussel","year":"2011","journal-title":"Journal of Satisfiability, Boolean Modeling and Computation"},{"key":"10.3233\/AIC-230325_ref24","doi-asserted-by":"crossref","unstructured":"P.\u00a0R\u00fcmmer, A constraint sequent calculus for first-order logic with linear integer arithmetic, in: Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, I.\u00a0Cervesato, H.\u00a0Veith and A.\u00a0Voronkov, eds, Lecture Notes in Artificial Intelligence, Springer-Verlag, 2008, pp.\u00a0274\u2013289.","DOI":"10.1007\/978-3-540-89439-1_20"},{"key":"10.3233\/AIC-230325_ref25","doi-asserted-by":"crossref","unstructured":"A.\u00a0Steen, G.\u00a0Sutcliffe, P.\u00a0Fontaine and J.\u00a0McKeown, Representation, verification, and visualization of tarskian interpretations for typed first-order logic, in: Proceedings of 24th International Conference on Logic for Programming Artificial Intelligence and Reasoning, R.\u00a0Piskac and A.\u00a0Voronkov, eds, EPiC Series in Computing, EasyChair Publications, 2023, pp.\u00a0369\u2013385.","DOI":"10.29007\/1rhx"},{"key":"10.3233\/AIC-230325_ref26","unstructured":"C.\u00a0Sticksel and K.\u00a0Korovin, A note on model representation and proof extraction in the first-order instantiation-based calculus inst-gen, in: Proceedings of the 19th Automated Reasoning Workshop, R.\u00a0Schmidt and F.\u00a0Papacchini, eds, 2012, pp.\u00a011\u201312."},{"key":"10.3233\/AIC-230325_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08587-6_28"},{"key":"10.3233\/AIC-230325_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-10769-6_38"},{"issue":"3","key":"10.3233\/AIC-230325_ref29","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1023\/A:1006393501098","article-title":"The CADE-16 ATP system competition","volume":"24","author":"Sutcliffe","year":"2000","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"10.3233\/AIC-230325_ref30","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1609\/aimag.v37i2.2620","article-title":"The CADE ATP system competition\u00a0\u2013 CASC","volume":"37","author":"Sutcliffe","year":"2016","journal-title":"AI Magazine"},{"issue":"4","key":"10.3233\/AIC-230325_ref31","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","article-title":"The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0","volume":"59","author":"Sutcliffe","year":"2017","journal-title":"Journal of Automated Reasoning"},{"issue":"6","key":"10.3233\/AIC-230325_ref32","doi-asserted-by":"crossref","first-page":"419","DOI":"10.3233\/AIC-170744","article-title":"The CADE-26 Automated Theorem Proving system competition\u00a0\u2013 CASC-26","volume":"30","author":"Sutcliffe","year":"2017","journal-title":"AI Communications"},{"key":"10.3233\/AIC-230325_ref33","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzac068"},{"issue":"2","key":"10.3233\/AIC-230325_ref35","doi-asserted-by":"publisher","first-page":"73","DOI":"10.3233\/AIC-220244","article-title":"The 11th IJCAR Automated Theorem Proving system competition\u00a0\u2013 CASC-J11","volume":"36","author":"Sutcliffe","year":"2023","journal-title":"AI Communications"},{"key":"10.3233\/AIC-230325_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_7"},{"issue":"1\u20132","key":"10.3233\/AIC-230325_ref37","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/S0004-3702(01)00113-8","article-title":"Evaluating general purpose Automated Theorem Proving systems","volume":"131","author":"Sutcliffe","year":"2001","journal-title":"Artificial Intelligence"},{"key":"10.3233\/AIC-230325_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_46"},{"key":"10.3233\/AIC-230325_ref39","unstructured":"A.\u00a0Voronkov, Spider: Learning in the Sea of Options, 2023, https:\/\/easychair.org\/smart-program\/Vampire23\/2023-07-05.html."},{"key":"10.3233\/AIC-230325_ref40","unstructured":"P.\u00a0Vukmirovi\u0107, A.\u00a0Bentkamp and V.\u00a0Nummelin, Efficient full higher-order unification, in: Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, Z.M.\u00a0Ariola, ed., Leibniz International Proceedings in Informatics, Dagstuhl Publishing, 2020, pp.\u00a05:1\u20135:20."},{"key":"10.3233\/AIC-230325_ref41","doi-asserted-by":"crossref","unstructured":"S.\u00a0Winkler and G.\u00a0Moser, MaedMax: A maximal ordered completion tool, in: Proceedings of the 9th International Joint Conference on Automated Reasoning, D.\u00a0Galmiche, S.\u00a0Schulz and R.\u00a0Sebastiani, eds, Lecture Notes in Computer Science, 2018, pp.\u00a0388\u2013404.","DOI":"10.1007\/978-3-319-94205-6_31"}],"container-title":["AI Communications"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/AIC-230325","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T18:28:18Z","timestamp":1777400898000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.medra.org\/servlet\/aliasResolver?alias=iospress&doi=10.3233\/AIC-230325"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,18]]},"references-count":39,"journal-issue":{"issue":"4"},"URL":"https:\/\/doi.org\/10.3233\/aic-230325","relation":{},"ISSN":["1875-8452","0921-7126"],"issn-type":[{"value":"1875-8452","type":"electronic"},{"value":"0921-7126","type":"print"}],"subject":[],"published":{"date-parts":[[2024,9,18]]}}}