The CADE-29 Automated Theorem Proving System Competition – CASC-29
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.
References
[1]
A. Bhayat, M. Rawson and J. Schoisswohl, Superposition with delayed unification, in: Proceedings of the 29th International Conference on Automated Deduction, B. Pientka and C. Tinelli, eds, Lecture Notes in Computer Science, Springer-Verlag, 2023, pp. 23–40.
[2]
A. Bhayat and G. Reger, A combinator-based superposition calculus for higher-order logic, in: Proceedings of the 10th International Joint Conference on Automated Reasoning, N. Peltier and V. Sofronie-Stokkermans, eds, Lecture Notes in Artificial Intelligence, 2020, pp. 278–296.
[3]
J. Blanchette, M. Haslbeck, D. Matichuk and T. Nipkow, Mining the archive of formal proofs, in: Proceedings of the 8th Conference on Intelligent Computer Mathematics, M. Kerber, J. Carette, C. Kaliszyk, F. Rabe and V. Sorge, eds, Lecture Notes in Computer Science, 2015, pp. 3–17.
[4]
J. Blanchette and T. 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, M. Kaufmann and L. Paulson, eds, Lecture Notes in Computer Science, Springer-Verlag, 2010, pp. 131–146.
[5]
F. Bobot, M. Bromberger and J. Hoenicke, 18th International Satisfiability Modulo Theories Competition (SMT-COMP 2023): Rules and Procedures, 2023, https://smt-comp.github.io/2023/rules.pdf.
[6]
F. Bobot, J.-C. Filliâtre, C. Marché and A. Paskevich, Let’s verify this with Why3, International Journal on Software Tools for Technology Transfer 17(6) (2015), 709–727.
[7]
K. Claessen and N. Sörensson, New techniques that improve MACE-style finite model finding, in: Proceedings of the CADE-19 Workshop: Model Computation – Principles, Algorithms, Applications, P. Baumgartner and C. Fermueller, eds, 2003.
[8]
L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language, in: Proceedings of the 28th International Conference on Automated Deduction, A. Platzer and G. Sutcliffe, eds, Lecture Notes in Computer Science, Springer-Verlag, 2015, pp. 625–635.
[9]
M. Desharnais, P. Vukmirović, J. Blanchette and M. Wnezel, Seventeen provers under the Hammer, in: Proceedings of the 13th International Conference on Interactive Theorem Proving, J. Andronick and L. de Moura, eds, Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022, pp. 8:1–8:18.
[10]
H. Ganzinger, C. Meyer and C. 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]
B. Gleiss and M. Suda, Layered clause selection for theory reasoning, in: Proceedings of the 10th International Joint Conference on Automated Reasoning, N. Peltier and V. Sofronie-Stokkermans, eds, Lecture Notes in Computer Science, 2020, pp. 402–409.
[12]
K. Hoder, G. Reger, M. Suda and A. Voronkov, Selecting the selection, in: Proceedings of the 8th International Joint Conference on Automated Reasoning, N. Olivetti and A. Tiwari, eds, Lecture Notes in Artificial Intelligence, 2016, pp. 313–329.
[13]
J. Jakubuv and J. Urban, ENIGMA: Efficient learning-based inference guiding machine, in: Proceedings of the 10th International Conference on Intelligent Computer Mathematics, H. Geuvers, M. England, O. Hasan, F. Rabe and O. Teschke, eds, Lecture Notes in Artificial Intelligence, Springer-Verlag, 2017, pp. 292–302.
[14]
K. Korovin, L. Kovac, G. Reger, J. Schoisswohl and A. Voronkov, ALASCA: Reasoning in quantified linear arithmetic (extended version), EasyChair preprints, 2023, https://easychair.org/publications/preprint/KJX2.
[15]
L. Kovacs and A. Voronkov, First-order theorem proving and vampire, in: Proceedings of the 25th International Conference on Computer Aided Verification, N. Sharygina and H. Veith, eds, Lecture Notes in Artificial Intelligence, Springer-Verlag, 2013, pp. 1–35.
[16]
U. Martin and T. 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.
[17]
J. McKeown and G. Sutcliffe, An interactive interpretation viewer for typed first-order logic, in: Proceedings of the 36th International FLAIRS Conference, A. Ae Chun and M. Franklin, eds, 2023.
[18]
J. Parsert, C. Brown, M. Janota and C. Kaliszyk, Experiments on infinite model finding in SMT solving, in: Proceedings of 24th International Conference on Logic for Programming Artificial Intelligence and Reasoning, R. Piskac and A. Voronkov, eds, EPiC Series in Computing, EasyChair Publications, 2023, pp. 317–328.
[19]
L. Paulson and J. 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, G. Sutcliffe, E. Ternovska and S. Schulz, eds, EPiC Series in Computing, EasyChair Publications, 2010, pp. 1–11.
[20]
F.J. Pelletier, G. Sutcliffe and C.B. Suttner, The development of CASC, AI Communications 15(2–3) (2002), 79–90.
[21]
A. Riazanov and A. Voronkov, Limited resource strategy in resolution theorem proving, Journal of Symbolic Computation 36(1–2) (2003), 101–115.
[22]
A. Robinson and A. Voronkov, Handbook of Automated Reasoning, Elsevier Science, 2001.
[23]
O. Roussel, Controlling a solver execution with the runsolver tool, Journal of Satisfiability, Boolean Modeling and Computation 7(4) (2011), 139–144.
[24]
P. 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, I. Cervesato, H. Veith and A. Voronkov, eds, Lecture Notes in Artificial Intelligence, Springer-Verlag, 2008, pp. 274–289.
[25]
A. Steen, G. Sutcliffe, P. Fontaine and J. 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, R. Piskac and A. Voronkov, eds, EPiC Series in Computing, EasyChair Publications, 2023, pp. 369–385.
[26]
C. Sticksel and K. 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, R. Schmidt and F. Papacchini, eds, 2012, pp. 11–12.
[27]
A. Stump, G. Sutcliffe and C. Tinelli, StarExec: A cross-community infrastructure for logic solving, in: Proceedings of the 7th International Joint Conference on Automated Reasoning, S. Demri, D. Kapur and C. Weidenbach, eds, Lecture Notes in Artificial Intelligence, 2014, pp. 367–373.
[28]
M. Suda, Vampire getting noisy: Will random bits help conquer chaos? (system description), in: Proceedings of the 11th International Joint Conference on Automated Reasoning, J. Blanchette, L. Kovacs and D. Pattinson, eds, Lecture Notes in Artificial Intelligence, 2022, pp. 659–667.
[29]
G. Sutcliffe, The CADE-16 ATP system competition, Journal of Automated Reasoning 24(3) (2000), 371–396.
[30]
G. Sutcliffe, The CADE ATP system competition – CASC, AI Magazine 37(2) (2016), 99–101.
[31]
G. 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.
[32]
G. Sutcliffe, The CADE-26 Automated Theorem Proving system competition – CASC-26, AI Communications 30(6) (2017), 419–432.
[33]
G. Sutcliffe, The logic languages of the TPTP world, Logic Journal of the IGPL (2022).
[34]
G. Sutcliffe, Proceedings of the CADE-29 ATP system competition, online, 2023, http://tptp.org/CASC/29/Proceedings.pdf.
[35]
G. Sutcliffe and M. Desharnais, The 11th IJCAR Automated Theorem Proving system competition – CASC-J11, AI Communications 36(2) (2023), 73–91.
[36]
G. Sutcliffe, S. Schulz, K. Claessen and A. Van Gelder, Using the TPTP language for writing derivations and finite interpretations, in: Proceedings of the 3rd International Joint Conference on Automated Reasoning, U. Furbach and N. Shankar, eds, Lecture Notes in Artificial Intelligence, Springer, 2006, pp. 67–81.
[37]
G. Sutcliffe and C.B. Suttner, Evaluating general purpose Automated Theorem Proving systems, Artificial Intelligence 131(1–2) (2001), 39–54.
[38]
A. Voronkov, AVATAR: The new architecture for first-order theorem provers, in: Proceedings of the 26th International Conference on Computer Aided Verification, A. Biere and R. Bloem, eds, Lecture Notes in Computer Science, 2014, pp. 696–710.
[39]
A. Voronkov, Spider: Learning in the Sea of Options, 2023, https://easychair.org/smart-program/Vampire23/2023-07-05.html.
[40]
P. Vukmirović, A. Bentkamp and V. 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]
S. Winkler and G. Moser, MaedMax: A maximal ordered completion tool, in: Proceedings of the 9th International Joint Conference on Automated Reasoning, D. Galmiche, S. Schulz and R. Sebastiani, eds, Lecture Notes in Computer Science, 2018, pp. 388–404.
Index Terms
- The CADE-29 Automated Theorem Proving System Competition – CASC-29
Index terms have been assigned to the content through auto-classification.
Recommendations
The CADE-22 automated theorem proving system competition - CASC-22
The CADE ATP System Competition (CASC) is an annual evaluation of fully automatic, classical logic Automated Theorem Proving (ATP) systems. CASC-22 was the fourteenth competition in the CASC series. Twenty-nine ATP systems and system variants competed ...
The CADE-23 Automated Theorem Proving System Competition - CASC-23
The CADE ATP System Competition (CASC) is an annual evaluation of fully automatic, classical logic Automated Theorem Proving (ATP) systems. CASC-23 was the sixteenth competition in the CASC series. Thirty-six ATP systems and system variants competed in ...
The 6th IJCAR automated theorem proving system competition --CASC-J6
The CADE ATP System Competition CASC is an annual evaluation of fully automatic, classical logic Automated Theorem Proving ATP systems. CASC-J6 was the seventeenth competition in the CASC series. Thirty-two ATP systems and system variants competed in ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
© 2024 – IOS Press. All rights reserved.
Publisher
IOS Press
Netherlands
Publication History
Published: 18 September 2024
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 19 Dec 2024