{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,19]],"date-time":"2026-01-19T05:39:08Z","timestamp":1768801148926,"version":"3.49.0"},"reference-count":37,"publisher":"SAGE Publications","issue":"4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AIC"],"published-print":{"date-parts":[[2022,3,18]]},"abstract":"<jats:p>The CADE ATP System Competition (CASC) is the annual evaluation of fully automatic, classical logic Automated Theorem Proving (ATP) systems. CASC-28 was the twenty-sixth competition in the CASC series. Twenty-two ATP systems competed in the various competition divisions. This paper presents an outline of the competition design and a commentated summary of the results.<\/jats:p>","DOI":"10.3233\/aic-210235","type":"journal-article","created":{"date-parts":[[2022,3,18]],"date-time":"2022-03-18T16:10:17Z","timestamp":1647619817000},"page":"259-276","source":"Crossref","is-referenced-by-count":4,"title":["The CADE-28 Automated Theorem Proving System Competition\u00a0\u2013 CASC-28"],"prefix":"10.1177","volume":"34","author":[{"given":"Geoff","family":"Sutcliffe","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Miami, USA"}]},{"given":"Martin","family":"Desharnais","sequence":"additional","affiliation":[{"name":"Automation of Logic, Max Planck Institute for Informatics, Germany"}]}],"member":"179","reference":[{"issue":"3","key":"10.3233\/AIC-210235_ref1","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/BF00252180","article-title":"TPS: A theorem-proving system for classical type theory","volume":"16","author":"Andrews","year":"1996","journal-title":"Journal of Automated Reasoning"},{"issue":"4","key":"10.3233\/AIC-210235_ref2","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1016\/j.jal.2005.10.002","article-title":"TPS: A hybrid automatic-interactive system for developing proofs","volume":"4","author":"Andrews","year":"2006","journal-title":"Journal of Applied Logic"},{"issue":"1","key":"10.3233\/AIC-210235_ref3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0747-7171(88)80018-X","article-title":"Critical pair criteria for completion","volume":"6","author":"Bachmair","year":"1988","journal-title":"Journal of Symbolic Computation"},{"key":"10.3233\/AIC-210235_ref5","doi-asserted-by":"crossref","unstructured":"A.\u00a0Bentkamp, J.\u00a0Blanchette, S.\u00a0Tourret and P.\u00a0Vukmirovi\u0107, Superposition for full higher-order logic, in: Proceedings of the 28th International Conference on Automated Deduction, A.\u00a0Platzer and G.\u00a0Sutcliffe, eds, Lecture Notes in Computer Science, Springer-Verlag, 2021, pp.\u00a0396\u2013412.","DOI":"10.1007\/978-3-030-79876-5_23"},{"key":"10.3233\/AIC-210235_ref6","doi-asserted-by":"crossref","unstructured":"J.\u00a0Blanchette, P.\u00a0Fontaine, S.\u00a0Schulz and U.\u00a0Waldmann, Towards strong higher-order automation for fast interactive verification, in: Proceedings of the 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, G.\u00a0Reger and D.\u00a0Trayfel, eds, EPiC Series in Computing, EasyChair Publications, 2017, pp.\u00a016\u201323.","DOI":"10.29007\/3ngx"},{"key":"10.3233\/AIC-210235_ref7","doi-asserted-by":"crossref","unstructured":"C.E.\u00a0Brown, Satallax: An automated higher-order prover (system description), in: Proceedings of the 6th International Joint Conference on Automated Reasoning, B.\u00a0Gramlich, D.\u00a0Miller and U.\u00a0Sattler, eds, Lecture Notes in Artificial Intelligence, 2012, pp.\u00a0111\u2013117.","DOI":"10.1007\/978-3-642-31365-3_11"},{"key":"10.3233\/AIC-210235_ref8","doi-asserted-by":"crossref","unstructured":"K.\u00a0Claessen and N.\u00a0Smallbone, Efficient encodings of first-order horn formulas in equational logic, 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_26"},{"key":"10.3233\/AIC-210235_ref9","doi-asserted-by":"crossref","unstructured":"L.\u00a0de\u00a0Moura and N.\u00a0Bj\u00f8rner, Z3: An efficient SMT solver, in: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, C.\u00a0Ramakrishnan and J.\u00a0Rehof, eds, Lecture Notes in Artificial Intelligence, Springer-Verlag, 2008, pp.\u00a0337\u2013340.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"10.3233\/AIC-210235_ref10","doi-asserted-by":"crossref","unstructured":"A.\u00a0Duarte and K.\u00a0Korovin, Implementing superposition in iProver, in: Proceedings of the 10th International Joint Conference on Automated Reasoning, N.\u00a0Peltier and V.\u00a0Sofronie-Stokkermans, eds, Lecture Notes in Artificial Intelligence, 2020, pp.\u00a0388\u2013397.","DOI":"10.1007\/978-3-030-51054-1_24"},{"key":"10.3233\/AIC-210235_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-86059-2_12"},{"key":"10.3233\/AIC-210235_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"10.3233\/AIC-210235_ref13","doi-asserted-by":"crossref","unstructured":"J.\u00a0Hernandez and K.\u00a0Korovin, An abstraction-refinement framework for reasoning with large theories, 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.\u00a0663\u2013679.","DOI":"10.1007\/978-3-319-94205-6_43"},{"key":"10.3233\/AIC-210235_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48660-7_20"},{"key":"10.3233\/AIC-210235_ref15","unstructured":"E.\u00a0Holden and K.\u00a0Korovin, SMAC and XGBoost your theorem prover, in: Proceedings of the 4th Conference on Artificial Intelligence and Theorem Proving, T.\u00a0Hales, C.\u00a0Kaliszyk, R.\u00a0Kumar, S.\u00a0Schulz and J.\u00a0Urban, eds, 2019, pp.\u00a093\u201395."},{"key":"10.3233\/AIC-210235_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81097-9_8"},{"key":"10.3233\/AIC-210235_ref17","doi-asserted-by":"crossref","unstructured":"K.\u00a0Korovin, iProver\u00a0\u2013 an instantiation-based theorem prover for first-order logic (system description), in: Proceedings of the 4th International Joint Conference on Automated Reasoning, P.\u00a0Baumgartner, A.\u00a0Armando and G.\u00a0Dowek, eds, Lecture Notes in Artificial Intelligence, 2008, pp.\u00a0292\u2013298.","DOI":"10.1007\/978-3-540-71070-7_24"},{"key":"10.3233\/AIC-210235_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37651-1_10"},{"key":"10.3233\/AIC-210235_ref19","doi-asserted-by":"crossref","unstructured":"E.\u00a0Kotelnikov, L.\u00a0Kovacs, M.\u00a0Suda and A.\u00a0Voronkov, A clausal normal form translation for FOOL, in: Proceedings of the 2nd Global Conference on Artificial Intelligence, C.\u00a0Benzm\u00fcller, G.\u00a0Sutcliffe and R.\u00a0Rojas, eds, EPiC Series in Computing, EasyChair Publications, 2016, pp.\u00a053\u201371.","DOI":"10.29007\/ltkk"},{"key":"10.3233\/AIC-210235_ref20","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-210235_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52885-7_100"},{"key":"10.3233\/AIC-210235_ref22","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"},{"key":"10.3233\/AIC-210235_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294100"},{"issue":"7","key":"10.3233\/AIC-210235_ref24","doi-asserted-by":"publisher","first-page":"1169","DOI":"10.1007\/s10817-020-09561-0","article-title":"Formalizing Bachmair and Ganzinger\u2019s ordered resolution prover","volume":"64","author":"Schlichtkrull","year":"2020","journal-title":"Journal of Automated Reasoning"},{"key":"10.3233\/AIC-210235_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36675-8_3"},{"key":"10.3233\/AIC-210235_ref26","doi-asserted-by":"crossref","unstructured":"S.\u00a0Schulz, S.\u00a0Cruanes and P.\u00a0Vukmirovic, Faster, higher, stronger: E 2.3, in: Proceedings of the 27th International Conference on Automated Deduction, P.\u00a0Fontaine, ed., Lecture Notes in Computer Science, Springer-Verlag, 2019, pp.\u00a0495\u2013507.","DOI":"10.1007\/978-3-030-29436-6_29"},{"key":"10.3233\/AIC-210235_ref27","doi-asserted-by":"crossref","unstructured":"N.\u00a0Smallbone, Twee: An equational theorem prover (system description), in: Proceedings of the 28th International Conference on Automated Deduction, A.\u00a0Platzer and G.\u00a0Sutcliffe, eds, Lecture Notes in Computer Science, Springer-Verlag, 2021, pp.\u00a0602\u2013613.","DOI":"10.1007\/978-3-030-79876-5_35"},{"key":"10.3233\/AIC-210235_ref28","doi-asserted-by":"crossref","unstructured":"A.\u00a0Stump, G.\u00a0Sutcliffe and C.\u00a0Tinelli, StarExec: A cross-community infrastructure for logic solving, in: Proceedings of the 7th International Joint Conference on Automated Reasoning, S.\u00a0Demri, D.\u00a0Kapur and C.\u00a0Weidenbach, eds, Lecture Notes in Artificial Intelligence, 2014, pp.\u00a0367\u2013373.","DOI":"10.1007\/978-3-319-08587-6_28"},{"issue":"3","key":"10.3233\/AIC-210235_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":"4","key":"10.3233\/AIC-210235_ref30","doi-asserted-by":"publisher","first-page":"683","DOI":"10.3233\/AIC-150668","article-title":"The 7th IJCAR automated theorem proving system competition\u00a0\u2013 CASC-J7","volume":"28","author":"Sutcliffe","year":"2015","journal-title":"AI Communications"},{"issue":"2","key":"10.3233\/AIC-210235_ref31","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-210235_ref32","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":"5\u20136","key":"10.3233\/AIC-210235_ref33","doi-asserted-by":"publisher","first-page":"373","DOI":"10.3233\/AIC-190627","article-title":"The CADE-27 automated theorem proving system competition\u00a0\u2013 CASC-27","volume":"32","author":"Sutcliffe","year":"2020","journal-title":"AI Communications"},{"issue":"2","key":"10.3233\/AIC-210235_ref34","doi-asserted-by":"publisher","first-page":"164","DOI":"10.3233\/AIC-201566","article-title":"The 10th IJCAR automated theorem proving system competition\u00a0\u2013 CASC-J10","volume":"34","author":"Sutcliffe","year":"2021","journal-title":"AI Communications"},{"issue":"1\u20132","key":"10.3233\/AIC-210235_ref36","doi-asserted-by":"publisher","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-210235_ref37","unstructured":"G.\u00a0Sutcliffe, J.\u00a0Zimmer and S.\u00a0Schulz, TSTP data-exchange formats for automated theorem proving tools, in: Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, W.\u00a0Zhang and V.\u00a0Sorge, eds, Frontiers in Artificial Intelligence and Applications, IOS Press, 2004, pp.\u00a0201\u2013215."},{"key":"10.3233\/AIC-210235_ref38","doi-asserted-by":"crossref","unstructured":"P.\u00a0Vukmirovi\u0107, A.\u00a0Bentkamp, J.\u00a0Blanchette, S.\u00a0Cruanes, V.\u00a0Nummelin and S.\u00a0Tourret, Making higher-order superposition work, in: Proceedings of the 28th International Conference on Automated Deduction, A.\u00a0Platzer and G.\u00a0Sutcliffe, eds, Lecture Notes in Computer Science, Springer-Verlag, 2021, pp.\u00a0415\u2013432.","DOI":"10.1007\/978-3-030-79876-5_24"},{"key":"10.3233\/AIC-210235_ref39","doi-asserted-by":"crossref","unstructured":"P.\u00a0Vukmirovic, J.\u00a0Blanchette, S.\u00a0Cruanes and S.\u00a0Schulz, Extending a brainiac prover to lambda-free higher-order logic, in: Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, T.\u00a0Vojnar and L.\u00a0Zhang, eds, Lecture Notes in Computer Science, Springer-Verlag, 2019, pp.\u00a0192\u2013210.","DOI":"10.1007\/978-3-030-17462-0_11"}],"container-title":["AI Communications"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/AIC-210235","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,11]],"date-time":"2025-03-11T05:50:18Z","timestamp":1741672218000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/AIC-210235"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,3,18]]},"references-count":37,"journal-issue":{"issue":"4"},"URL":"https:\/\/doi.org\/10.3233\/aic-210235","relation":{},"ISSN":["1875-8452","0921-7126"],"issn-type":[{"value":"1875-8452","type":"electronic"},{"value":"0921-7126","type":"print"}],"subject":[],"published":{"date-parts":[[2022,3,18]]}}}