Sage Journals: Discover world-class research

Abstract

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-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.

Keywords

Automated Theorem Proving competition

Get full access to this article

View all access options for this article.

References

Bhayat ,

Rawson and

Schoisswohl , Superposition with delayed unification, in: Proceedings of the 29th International Conference on Automated Deduction,

Pientka and

Tinelli , eds, Lecture Notes in Computer Science, Springer-Verlag, 2023, pp. 23–40.

Bhayat and

Reger , A combinator-based superposition calculus for higher-order logic, in: Proceedings of the 10th International Joint Conference on Automated Reasoning,

Peltier and

Sofronie-Stokkermans , eds, Lecture Notes in Artificial Intelligence, 2020, pp. 278–296. doi:10.1007/978-3-030-51074-9_16.

Blanchette ,

Haslbeck ,

Matichuk and

Nipkow , Mining the archive of formal proofs, in: Proceedings of the 8th Conference on Intelligent Computer Mathematics,

Kerber ,

Carette ,

Kaliszyk ,

Rabe and

Sorge , eds, Lecture Notes in Computer Science, 2015, pp. 3–17. doi:10.1007/978-3-319-20615-8_1.

Blanchette and

Nipkow , Nitpick: A counterexample generator for higher-order logic based on a relational model finder, in: Proceedings of the 1st International Conference on Interactive Theorem Proving,

Kaufmann and

Paulson , eds, Lecture Notes in Computer Science, Springer-Verlag, 2010, pp. 131–146. doi:10.1007/978-3-642-14052-5_11.

Bobot ,

Bromberger and

Hoenicke , 18th International Satisfiability Modulo Theories Competition (SMT-COMP 2023): Rules and Procedures, 2023, https://smt-comp.github.io/2023/rules.pdf .

Bobot ,

J.-C.

Filliâtre ,

Marché and

Paskevich , Let’s verify this with Why3, International Journal on Software Tools for Technology Transfer 17(6) (2015), 709–727. doi:10.1007/s10009-014-0314-5.

Claessen and

Sörensson , New techniques that improve MACE-style finite model finding, in: Proceedings of the CADE-19 Workshop: Model Computation – Principles, Algorithms, Applications,

Baumgartner and

Fermueller , eds, 2003.

de Moura and

Ullrich , The Lean 4 theorem prover and programming language, in: Proceedings of the 28th International Conference on Automated Deduction,

Platzer and

Sutcliffe , eds, Lecture Notes in Computer Science, Springer-Verlag, 2015, pp. 625–635.

Desharnais ,

Vukmirović ,

Blanchette and

Wnezel , Seventeen provers under the Hammer, in: Proceedings of the 13th International Conference on Interactive Theorem Proving,

Andronick and

de Moura , eds, Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022, pp. 8:1–8:18.

10.

Ganzinger ,

Meyer and

Weidenbach , Soft typing for ordered resolution, in: Proceedings of the 14th International Conference on Automated Deduction,

W.W.

McCune , ed., Lecture Notes in Artificial Intelligence, Springer-Verlag, 1997, pp. 321–335.

11.

Gleiss and

Suda , Layered clause selection for theory reasoning, in: Proceedings of the 10th International Joint Conference on Automated Reasoning,

Peltier and

Sofronie-Stokkermans , eds, Lecture Notes in Computer Science, 2020, pp. 402–409. doi:10.1007/978-3-030-51074-9_23.

12.

Hoder ,

Reger ,

Suda and

Voronkov , Selecting the selection, in: Proceedings of the 8th International Joint Conference on Automated Reasoning,

Olivetti and

Tiwari , eds, Lecture Notes in Artificial Intelligence, 2016, pp. 313–329. doi:10.1007/978-3-319-40229-1_22.

13.

Jakubuv and

Urban , ENIGMA: Efficient learning-based inference guiding machine, in: Proceedings of the 10th International Conference on Intelligent Computer Mathematics,

Geuvers ,

England ,

Hasan ,

Rabe and

Teschke , eds, Lecture Notes in Artificial Intelligence, Springer-Verlag, 2017, pp. 292–302.

14.

Korovin ,

Kovac ,

Reger ,

Schoisswohl and

Voronkov , ALASCA: Reasoning in quantified linear arithmetic (extended version), EasyChair preprints, 2023, https://easychair.org/publications/preprint/KJX2.

15.

Kovacs and

Voronkov , First-order theorem proving and vampire, in: Proceedings of the 25th International Conference on Computer Aided Verification,

Sharygina and

Veith , eds, Lecture Notes in Artificial Intelligence, Springer-Verlag, 2013, pp. 1–35.

16.

Martin and

Nipkow , Ordered rewriting and confluence, in: Proceedings of the 10th International Conference on Automated Deduction,

M.E.

Stickel , ed., Lecture Notes in Artificial Intelligence, Springer-Verlag, 1990, pp. 366–380. doi:10.1007/3-540-52885-7_100.

17.

McKeown and

Sutcliffe , An interactive interpretation viewer for typed first-order logic, in: Proceedings of the 36th International FLAIRS Conference,

Ae Chun and

Franklin , eds, 2023. doi:10.32473/flairs.36.133073.

18.

Parsert ,

Brown ,

Janota and

Kaliszyk , Experiments on infinite model finding in SMT solving, in: Proceedings of 24th International Conference on Logic for Programming Artificial Intelligence and Reasoning,

Piskac and

Voronkov , eds, EPiC Series in Computing, EasyChair Publications, 2023, pp. 317–328.

19.

Paulson and

Blanchette , 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,

Sutcliffe ,

Ternovska and

Schulz , eds, EPiC Series in Computing, EasyChair Publications, 2010, pp. 1–11.

20.

F.J.

Pelletier ,

Sutcliffe and

C.B.

Suttner , The development of CASC, AI Communications 15(2–3) (2002), 79–90.

21.

Riazanov and

Voronkov , Limited resource strategy in resolution theorem proving, Journal of Symbolic Computation 36(1–2) (2003), 101–115. doi:10.1016/S0747-7171(03)00040-3.

22.

Robinson and

Voronkov , Handbook of Automated Reasoning, Elsevier Science, 2001.

23.

Roussel , Controlling a solver execution with the runsolver tool, Journal of Satisfiability, Boolean Modeling and Computation 7(4) (2011), 139–144. doi:10.3233/SAT190083.

24.

Rümmer , 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,

Cervesato ,

Veith and

Voronkov , eds, Lecture Notes in Artificial Intelligence, Springer-Verlag, 2008, pp. 274–289.

25.

Steen ,

Sutcliffe ,

Fontaine and

McKeown , 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,

Piskac and

Voronkov , eds, EPiC Series in Computing, EasyChair Publications, 2023, pp. 369–385.

26.

Sticksel and

Korovin , 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,

Schmidt and

Papacchini , eds, 2012, pp. 11–12.

27.

Stump ,

Sutcliffe and

Tinelli , StarExec: A cross-community infrastructure for logic solving, in: Proceedings of the 7th International Joint Conference on Automated Reasoning,

Demri ,

Kapur and

Weidenbach , eds, Lecture Notes in Artificial Intelligence, 2014, pp. 367–373. doi:10.1007/978-3-319-08587-6_28.

28.

Suda , Vampire getting noisy: Will random bits help conquer chaos? (system description), in: Proceedings of the 11th International Joint Conference on Automated Reasoning,

Blanchette ,

Kovacs and

Pattinson , eds, Lecture Notes in Artificial Intelligence, 2022, pp. 659–667. doi:10.1007/978-3-031-10769-6_38.

29.

Sutcliffe , The CADE-16 ATP system competition, Journal of Automated Reasoning 24(3) (2000), 371–396. doi:10.1023/A:1006393501098.

30.

Sutcliffe , The CADE ATP system competition – CASC, AI Magazine 37(2) (2016), 99–101. doi:10.1609/aimag.v37i2.2620.

31.

Sutcliffe , The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0, Journal of Automated Reasoning 59(4) (2017), 483–502. doi:10.1007/s10817-017-9407-7.

32.

Sutcliffe , The CADE-26 Automated Theorem Proving system competition – CASC-26, AI Communications 30(6) (2017), 419–432.

33.

Sutcliffe , The logic languages of the TPTP world, Logic Journal of the IGPL (2022). doi:10.1093/jigpal/jzac068.

34.

Sutcliffe , Proceedings of the CADE-29 ATP system competition, online, 2023, http://tptp.org/CASC/29/Proceedings.pdf.

35.

Sutcliffe and

Desharnais , The 11th IJCAR Automated Theorem Proving system competition – CASC-J11, AI Communications 36(2) (2023), 73–91. doi:10.3233/AIC-220244.

36.

Sutcliffe ,

Schulz ,

Claessen and

Van Gelder , Using the TPTP language for writing derivations and finite interpretations, in: Proceedings of the 3rd International Joint Conference on Automated Reasoning,

Furbach and

Shankar , eds, Lecture Notes in Artificial Intelligence, Springer, 2006, pp. 67–81. doi:10.1007/11814771_7.

37.

Sutcliffe and

C.B.

Suttner , Evaluating general purpose Automated Theorem Proving systems, Artificial Intelligence 131(1–2) (2001), 39–54.

38.

Voronkov , AVATAR: The new architecture for first-order theorem provers, in: Proceedings of the 26th International Conference on Computer Aided Verification,

Biere and

Bloem , eds, Lecture Notes in Computer Science, 2014, pp. 696–710. doi:10.1007/978-3-319-08867-9_46.

39.

Voronkov , Spider: Learning in the Sea of Options, 2023, https://easychair.org/smart-program/Vampire23/2023-07-05.html.

40.

Vukmirović ,

Bentkamp and

Nummelin , Efficient full higher-order unification, in: Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction,

Z.M.

Ariola , ed., Leibniz International Proceedings in Informatics, Dagstuhl Publishing, 2020, pp. 5:1–5:20.

41.

Winkler and

Moser , MaedMax: A maximal ordered completion tool, in: Proceedings of the 9th International Joint Conference on Automated Reasoning,

Galmiche ,

Schulz and

Sebastiani , eds, Lecture Notes in Computer Science, 2018, pp. 388–404.

The CADE-29 Automated Theorem Proving System Competition – CASC-29

Abstract

Keywords

Get full access to this article

References