The CADE ATP System Competition (CASC) is the annual evaluation of fully automatic, classical logic Automated Theorem Proving (ATP) systems. CASC-J10 was the twenty-fifth competition in the CASC series. Twenty-four ATP systems and system variants competed in the various competition divisions. This paper presents an outline of the competition design, and a commentated summary of the results.
J.Alama, T.Heskes, D.Külwein, E.Tsivtsivadze and J.Urban, Premise selection for mathematics by corpus analysis and kernel methods, Journal of Automated Reasoning52(2) (2014), 191–213. doi:10.1007/s10817-013-9286-5.
2.
A.Bentkamp, J.Blanchette, P.Vukmirovic and U.Waldmann, Superposition with lambdas, in: Proceedings of the 27th International Conference on Automated Deduction, P.Fontaine, ed., Lecture Notes in Computer Science, Vol. 11716, Springer-Verlag, 2019, pp. 55–73.
3.
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, Vol. 12166, 2020, pp. 278–296.
4.
A.Bhayat and G.Reger, A Knuth-bendix-like ordering for orienting combinator equations, in: Proceedings of the 10th International Joint Conference on Automated Reasoning, N.Peltier and V.Sofronie-Stokkermans, eds, Lecture Notes in Artificial Intelligence, Vol. 12166, 2020, pp. 259–277.
5.
J.Blanchette, C.Kaliszyk, L.Paulson and J.Urban, Hammering towards QED, Journal of Formalized Reasoning9(1) (2016), 101–148.
6.
J.U.BliStr, The blind strategymaker, in: Proceedings of the 1st Global Conference on Artificial Intelligence, S.Autexier, ed., EPiC Series in Computing, Vol. 36, EasyChair Publications, 2015, pp. 312–319.
7.
C.Brown, T.Gauthier, C.Kaliszyk, G.Sutcliffe and J.Urban, GRUNGE: A grand unified ATP challenge, in: Proceedings of the 27th International Conference on Automated Deduction, P.Fontaine, ed., Lecture Notes in Computer Science, Vol. 11716, Springer-Verlag, 2019, pp. 123–141.
8.
K.Chvalovsky, J.Jakubuv, M.Suda and J.Urban, ENIGMA-NG: Efficient neural and gradient-boosted inference guidance for E, in: Proceedings of the 27th International Conference on Automated Deduction, P.Fontaine, ed., Lecture Notes in Computer Science, Vol. 11716, Springer-Verlag, 2019, pp. 197–215.
9.
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.
10.
B.Gleiss and M.Suda, Layered clause selection for saturation-based theorem proving, in: Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning, P.Fontaine, P.Rümmer and S.Tourret, eds, CEUR Workshop Proceedings, Vol. 2752, 2020, pp. 34–52.
11.
L.Gleiss, B.Kovacs and J.Rath, Subsumption demodulation in first-order theorem proving, in: Proceedings of the 10th International Joint Conference on Automated Reasoning, N.Peltier and V.Sofronie-Stokkermans, eds, Lecture Notes in Computer Science, Vol. 12166, 2020, pp. 297–315.
12.
J.Jakubuv, K.Chvalovský, M.Olsák, B.Piotrowski, M.Suda and J.Urban, ENIGMA anonymous: Symbol-independent inference guiding machine (system description), in: Proceedings of the 10th International Joint Conference on Automated Reasoning, N.Peltier and V.Sofronie-Stokkermans, eds, Lecture Notes in Artificial Intelligence, Vol. 12167, 2020, pp. 448–463.
13.
J.Jakubuv and J.Urban, Hierarchical invention of theorem proving strategies, AI Communications31(3) (2018), 237–250. doi:10.3233/AIC-180761.
14.
J.Jakubuv and J.Urban, Hammering mizar by learning clause guidance, in: Proceedings of the 10th International Conference on Interactive Theorem Proving, Leibniz International Proceedings in Informatics, Dagstuhl Publishing, 2019.
15.
C.Kaliszyk, J.Urban and J.Vyskocil, Machine learner for automated reasoning 0.4 and 0.5, in: Proceedings of the 4th Workshop on Practical Aspects of Automated Reasoning, S.Schulz, L.de Moura and B.Konev, eds, EPiC Series in Computing, Vol. 31, EasyChair Publications, 2015, pp. 60–66.
16.
T.Lampert and A.Nakano, Deciding simple infinity axiom sets with one binary relation by superpostulates, in: Proceedings of the 10th International Joint Conference on Automated Reasoning, N.Peltier and V.Sofronie-Stokkermans, eds, Lecture Notes in Artificial Intelligence, Vol. 12166, 2020, pp. 201–217.
17.
D.L.Li and A.Tiu, Combining ProVerif and automated theorem provers for security protocol verification, in: Proceedings of the 27th International Conference on Automated Deduction, P.Fontaine, ed., Lecture Notes in Computer Science, Vol. 11716, Springer-Verlag, 2019, pp. 354–365.
18.
A.Paskevich, Connection tableaux with lazy paramodulation, Journal of Automated Reasoning40(2–3) (2008), 179–194. doi:10.1007/s10817-007-9089-7.
19.
M.Rawson and G.Reger, 2020, lazyCoP 0.1. EasyChair Preprints 3926.
20.
A.Riazanov and A.Voronkov, Limited resource strategy in resolution theorem proving, Journal of Symbolic Computation36(1–2) (2003), 101–115. doi:10.1016/S0747-7171(03)00040-3.
21.
S.Schulz, E: A brainiac theorem prover, AI Communications15(2–3) (2002), 111–126.
22.
S.Schulz, G.Sutcliffe, J.Urban and A.Pease, Detecting inconsistencies in large first-order knowledge bases, in: Proceedings of the 26th International Conference on Automated Deduction, L.de Moura, ed., Lecture Notes in Computer Science, Vol. 10395, Springer-Verlag, 2017, pp. 310–325.
23.
K.Slind and M.Norrish, A brief overview of HOL4, in: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, O.Mohamed, C.Munoz and S.Tahar, eds, Lecture Notes in Computer Science, Vol. 5170, Springer-Verlag, 2008, pp. 28–32. doi:10.1007/978-3-540-71067-7_6.
24.
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, Vol. 8562, 2014, pp. 367–373.
25.
G.Sutcliffe, The CADE-16 ATP system competition, Journal of Automated Reasoning24(3) (2000), 371–396. doi:10.1023/A:1006393501098.
26.
G.Sutcliffe, The TPTP problem library and associated infrastructure. The FOF and CNF parts, v3.5.0, Journal of Automated Reasoning43(4) (2009), 337–362. doi:10.1007/s10817-009-9143-8.
27.
G.Sutcliffe, The CADE ATP system competition – CASC, AI Magazine37(2) (2016), 99–101. doi:10.1609/aimag.v37i2.2620.
28.
G.Sutcliffe, The CADE-26 automated theorem proving system competition – CASC-26, AI Communications30(6) (2017), 419–432. doi:10.3233/AIC-170744.
G.Sutcliffe, The CADE-27 automated theorem proving system competition – CASC-27, AI Communications32(5–6) (2020), 373–389. doi:10.3233/AIC-190627.
31.
G.Sutcliffe and F.J.Pelletier, Hoping for the truth – a survey of the TPTP logics, in: Proceedings of the 29th International FLAIRS Conference, Z.Markov and I.Russell, eds, 2016, pp. 110–115.
32.
G.Sutcliffe and C.B.Suttner, Evaluating general purpose automated theorem proving systems, Artificial Intelligence131(1–2) (2001), 39–54. doi:10.1016/S0004-3702(01)00113-8.
33.
P.Vukmirovic, 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, Vol. 167, Dagstuhl Publishing, 2020, pp. 5:1–5:20.
34.
P.Vukmirovic and V.Nummelin, Boolean reasoning in a higher-order superposition prover, in: Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning, P.Fontaine, P.Rümmer and S.Tourret, eds, CEUR Workshop Proceedings, Vol. 2752, 2020, pp. 148–166.
