The CADE ATP System Competition (CASC) is the annual evaluation of fully automatic, classical logic, Automated Theorem Proving (ATP) systems—the world championship for such systems. CASC-30 was the 30th competition in the CASC series. Nineteen ATP systems competed in the various divisions. This article presents an outline of the competition design and a commentated summary of the results.
AndreottiB.LachnittH.BarbosaH. (2023). Carcara: An efficient proof checker and elaborator for SMT proofs in the Alethe format. In S. Sankaranarayanan & N. Sharygina (Eds.), Proceedings of the 13th international conference on tools and algorithms for the construction and analysis of systems (Lecture Notes in Computer Science, pp. 367–386). Springer-Verlag.
2.
BártekF.ChvalovskýK.SudaS. (2024). Cautious specialization of strategy schedules. In C. W. Brown, D. Kaufmann, C. Nalon, A. Steen, & M. Suda (Eds.), Joint proceedings of the 9th workshop on practical aspects of automated reasoning and the 9th satisfiability checking and symbolic computation workshop (CEUR Workshop Proceedings, pp. 28–36).
3.
BeyerD.LöweS.WendlerP. (2019). Reliable benchmarking: Requirements and solutions. International Journal on Software Tools for Technology Transfer, 21, 1–29. 10.1007/s10009-017-0469-y
4.
BiereA. (2008). PicoSAT essentials. Journal on Satisfiability, Boolean Modeling and Computation, 4, 75–97. 10.3233/SAT190039
5.
BiereA.FallerT.FazekasK.FleuryM.FroleyksN.PollittF. (2024). CaDiCaL 2.0. In A. Gurfinkel & V. Ganesh (Eds.), Proceedings of the 36th international conference on computer aided verification (Lecture Notes in Computer Science, pp. 133–152). Springer-Verlag.
6.
BlanchetteJ.HaslbeckM.MatichukD.NipkowT. (2015). Mining the archive of formal proofs. In M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, & V. Sorge (Eds.), Proceedings of the 8th conference on intelligent computer mathematics (Lecture Notes in Computer Science, pp. 3–17). Springer-Verlag.
7.
BlanchetteJ.NipkowT. (2010). Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In M. Kaufmann & L. Paulson (Eds.), Proceedings of the 1st international conference on interactive theorem proving (Lecture Notes in Computer Science, pp. 131–146). Springer-Verlag.
8.
BrombergerM.KrasnopolF.MoehleS.WeidenbachC. (2024). First-order automatic literal model generation. In C. Benzmüller, M. Heule, & R. Schmidt (Eds.), Proceedings of the 12th international joint conference on automated reasoning (Lecture Notes in Artificial Intelligence, pp. 133–153).
9.
BrombergerM.SchwarzS.WeidenbachC. (2023). Exploring partial models with SCL. In, R. Piskac & A. Voronkov (Eds.), Proceedings of the 24th international conference on logic for programming, artificial intelligence, and reasoning (EPiC Series in Computing, pp. 48–72). EasyChair Publications.
10.
BrownC. (2024). Simple difficult problems for automated theorem provers.
11.
ClaessenK.SörenssonN. (2003). New techniques that improve MACE-style finite model finding. In P. Baumgartner & C. Fermueller (Eds.), Proceedings of the CADE-19 workshop: Model computation—Principles, algorithms, applications.
12.
de MouraL.BjørnerN. (2008). Z3: An efficient SMT solver. In C. Ramakrishnan & J. Rehof (Eds.), Proceedings of the 14th international conference on tools and algorithms for the construction and analysis of systems (Lecture Notes in Artificial Intelligence, pp. 337–340). Springer-Verlag.
EénN.SörenssonN. (2004). An extensible SAT-solver. In E. Giunchiglia & A. Tacchella (Eds.), Proceedings of the 6th international conference on theory and applications of satisfiability testing (Lecture Notes in Computer Science, pp. 502–518). Springer-Verlag.
15.
FichteJ.GeibingerT.HecherM.SchlögelM. (2024). Parallel empirical evaluations: Resilience despite concurrency. In M. Wooldridge, J. Dy, & S. Natarajan (Eds.), Proceedings of the 38th AAAI conference on artificial intelligence (Vol. 38, pp. 8004–8012). AAAI Press.
16.
GuilloudS.BucevM.MilovancevićD.KuncakV. (2023). Formula normalizations in verification. In C. Enea & A. Lal (Eds.), Proceedings of the 35th international conference on computer aided verification (Lecture Notes in Computer Science, pp. 398–422).
17.
GuilloudS.CallierJ.GambhirS.PoirouxA.HerklotzY.BourgeatT.KuncakV. (2025). Interoperability of proof systems with SC-TPTP. In C. Barrett & U. Waldmann (Eds.), Proceedings of the 30th international conference on automated deduction (Lecture Notes in Artificial Intelligence, pp. 325–340). Springer-Verlag.
18.
GuilloudS.GambhirS.KuncakV. (2023). LISA—A modern proof system. In A. Naumowicz & R. Thiemann (Eds.), Proceedings of the 14th international conference on interactive theorem proving (Leibniz International Proceedings in Informatics, pp. 17:1–17:19).
19.
GuilloudS.KuncakV. (2024). Orthologic with axioms. In M. Hicks (Ed.), Proceedings of the ACM on programming languages (Vol. 8, pp. 1150–1178). Association for Computing Machinery.
20.
HajduM.CoutelierR.KovácsL.VoronkovA. (2025). Term ordering diagrams. In C. Barrett & U. Waldmann (Eds.), Proceedings of the 30th international conference on automated deduction (Lecture Notes in Artificial Intelligence, pp. 552–569). Springer-Verlag.
21.
HajduM.KovácsL.VoronkovA. (2025). Partial redundancy in saturation. In C. Barrett & U. Waldmann (Eds.), Proceedings of the 30th international conference on automated deduction (Lecture Notes in Artificial Intelligence, pp. 532–551). Springer-Verlag.
22.
HoldenS. (2023). Connect++: A new automated theorem prover based on the connection calculus. In J. Otten & W. Bibel (Eds.), Proceedings of the 1st international workshop on automated reasoning with connection calculi (CEUR Workshop Proceedings, pp. 95–106).
23.
JakubuvJ.UrbanJ. (2017). ENIGMA: Efficient learning-based inference guiding machine. In H. Geuvers, M. England, O. Hasan, F. Rabe, & O. Teschke (Eds.), Proceedings of the 10th international conference on intelligent computer mathematics (Lecture Notes in Artificial Intelligence, pp. 292–302). Springer-Verlag.
24.
KorovinK.KovácsL.RegerG.SchoisswohlJ. (2023). ALASCA: Reasoning in quantified linear arithmetic. In S. Sankaranarayanan & N. Sharygina (Eds.), Proceedings of the 29th international conference on tools and algorithms for the construction and analysis of systems (Lecture Notes in Computer Science, pp. 647–665). Springer-Verlag.
25.
LetzR.SchumannJ.BayerlS.BibelW. (1992). SETHEO: A high-performance theorem prover. Journal of Automated Reasoning, 8(2), 183–212. 10.1007/BF00244282
26.
McCuneW.Shumsky-MatlinO. (2000). Ivy: A preprocessor and proof checker for first-order logic. In M. Kaufmann, P. Manolios, & J. Strother Moore (Eds.), Computer-aided reasoning: ACL2 case studies (Advances in Formal Methods, pp. 265–282). Kluwer Academic Publishers.
27.
MesnardF.MarianneT.PayetE. (2024). ATP for prolog verification. In N. Bjørner, M. Heule, & A. Voronkov (Eds.), Proceedings of the short papers of the 25th international conference on logic for programming, artificial intelligence, and reasoning (Kalpa Publications in Computing, pp. 137–151). EasyChair Publications.
28.
MuellerE.SutcliffeG. (2005). Reasoning in the event calculus using first-order automated theorem proving. In I. Russell & Z. Markov (Eds.), Proceedings of the 18th international flairs conference (pp. 840–841). AAAI Press.
PaulsonL.BlanchetteJ. (2010). Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In G. Sutcliffe, E. Ternovska, & S. Schulz (Eds.), Proceedings of the 8th international workshop on the implementation of logics (EPiC Series in Computing, pp. 1–11). EasyChair Publications.
31.
PeltierN. (2003). Model building with ordered resolution: Extracting models from saturated clause sets. Journal of Symbolic Computation, 36(1–2), 5–48. 10.1016/S0747-7171(03)00028-2
32.
RawsonM.WernhardC.ZomboriZ.BibelW. (2023). Lemmas: Generation, selection, application. In D. Ramanayake & J. Urban (Eds.), Proceedings of the 32nd international conference on automated reasoning with analytic tableaux and related methods (Lecture Notes in Computer Science, pp. 153–174).
33.
RobinsonA.VoronkovA. (2001). Handbook of automated reasoning. Elsevier Science.
34.
RousselO. (2011). Controlling a solver execution with the runsolver tool. Journal of Satisfiability, Boolean Modeling and Computation, 7(4), 139--144. 10.3233/SAT190083
35.
SchoisswohlJ.KovácsL.KorovinK. (2024). VIRAS: Conflict-driven quantifier elimination for integer-real arithmetic. In N. Bjørner, M. Heule, & A. Voronkov (Eds.), Proceedings of the 25th international conference on logic for programming, artificial intelligence, and reasoning (EPiC Series in Computing, pp. 147--164). EasyChair Publications.
36.
SteenA.SutcliffeG.FontaineP.McKeownJ. (2023). Representation, verification, and visualization of tarskian interpretations for typed first-order logic. In R. Piskac & A. Voronkov (Eds.), Proceedings of 24th international conference on logic for programming artificial intelligence and reasoning (EPiC Series in Computing, pp. 369--385). EasyChair Publications.
37.
StumpA.SutcliffeG.TinelliC. (2014). StarExec: A cross-community infrastructure for logic solving. In S. Demri, D. Kapur, & C. Weidenbach (Eds.), Proceedings of the 7th international joint conference on automated reasoning (Lecture Notes in Artificial Intelligence, pp. 367--373).
38.
SutcliffeG. (2000). The CADE-16 ATP system competition. Journal of Automated Reasoning, 24(3), 371--396. 10.1023/A:1006393501098
39.
SutcliffeG. (2007). TPTP, TSTP, CASC, etc. In V. Diekert, M. Volkov, & A. Voronkov (Eds.), Proceedings of the 2nd international symposium on computer science in Russia (Lecture Notes in Computer Science, pp. 6--22). Springer-Verlag.
40.
SutcliffeG. (2016). The CADE ATP system competition---CASC. AI Magazine, 37(2), 99--101. 10.1609/aimag.v37i2.2620
41.
SutcliffeG. (2017). The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. Journal of Automated Reasoning, 59(4), 483--502. 10.1007/s10817-017-9407-7
SutcliffeG. (2024b). Stepping stones in the TPTP world. In C. Benzmüller, M. Heule, & R. Schmidt (Eds.), Proceedings of the 12th international joint conference on automated reasoning (Lecture Notes in Artificial Intelligence, pp. 30--50).
46.
SutcliffeG. (2025a). The 12th IJCAR automated theorem proving system competition---CASC-J12. AI Communications, 38(1), 3--20. 10.1177/30504554241305110
SutcliffeG.BelfioreD. (2005). Semantic derivation verification. In I. Russell & Z. Markov (Eds.), Proceedings of the 18th international flairs conference (pp. 641--646). AAAI Press.
49.
SutcliffeG.DesharnaisM. (2024). The CADE-29 atutomated theorem proving system competition---CASC-29. AI Communications, 37(4), 485--503. 10.3233/AIC-230325
50.
SutcliffeG.SchulzS.ClaessenK.Van GelderA. (2006). Using the TPTP language for writing derivations and finite interpretations. In U. Furbach & N. Shankar (Eds.), Proceedings of the 3rd international joint conference on automated reasoning (Lecture Notes in Artificial Intelligence, pp. 67--81), Springer.
51.
SutcliffeG.SuttnerC. B. (2001). Evaluating general purpose automated theorem proving systems. Artificial Intelligence, 131(1--2), 39--54. 10.1016/S0004-3702(01)00113-8
52.
WetzlerN.HeuleM.HuntW. (2014). DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In C. Sinz & U. Egly (Eds.), Proceedings of the 17th international conference on the theory and applications of satisfiability testing (Lecture Notes in Theoretical Computer Science, pp. 422--429). Springer-Verlag.
