The CADE ATP System Competition (CASC) is the annual evaluation of fully automatic, classical logic Automated Theorem Proving (ATP) systems. CASC-J8 was the twenty-first competition in the CASC series. Twenty-one ATP systems and system variants competed in the various competition divisions. An outline of the competition design, and a commentated summary of the results, are presented.
T.Gauthier and C.Kaliszyk, Premise selection and external provers for HOL4, in: Proceedings of the 4th ACM SIGPLAN Conference on Certified Programs and Proofs, X.Leroy and A.Tiu, eds, ACM Press, 2015, pp. 49–57.
2.
T.Hales, A revision of the proof of the Kepler conjecture, Discrete and Computational Geometry44(1) (2010), 1–34. doi:10.1007/s00454-009-9148-4.
3.
K.Hoder and A.Voronkov, Sine qua non for large theory reasoning, in: Proceedings of the 23rd International Conference on Automated Deduction, V.Sofronie-Stokkermans and N.Bjœrner, eds, Lecture Notes in Artificial Intelligence, Vol. 6803, Springer-Verlag, 2011, pp. 299–314.
4.
J.Harrison, HOL light: An overview, in: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, T.Nipkow and C.Urban, eds, Lecture Notes in Computer Science, Vol. 5674, Springer-Verlag, 2009, pp. 60–66.
5.
C.Kaliszyk, G.Sutcliffe and F.Rabe, TH1: The TPTP typed higher-order form with rank-1 polymorphism, in: Proceedings of the 5th Workshop on the Practical Aspects of Automated Reasoning, P.Fontaine, S.Schulz and J.Urban, eds, CEUR Workshop Proceedings, Vol. 1653, 2016, pp. 41–55.
6.
Z.Khasidashvili and K.Korovin, Predicate elimination for preprocessing in first-order theorem proving, in: Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing, N.Creignou and D.Le Berre, eds, Lecture Notes in Computer Science, Vol. 9710, Springer-Verlag, 2016, pp. 361–372.
7.
M.Kinyon, R.Veroff and P.Vojtechovsky, Loops with Abelian inner mapping groups: An application of automated deduction, in: Automated Reasoning and Mathematics: Essays in Memory of William W. McCune, M.P.Bonacina and M.Stickel, eds, Lecture Notes in Artificial Intelligence, Vol. 7788, Springer-Verlag, 2013, pp. 151–164. doi:10.1007/978-3-642-36675-8_8.
8.
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, Vol. 8044, Springer-Verlag, 2013, pp. 1–35. doi:10.1007/978-3-642-39799-8_1.
9.
R.Kumar, M.Myreen, M.Norrish and S.Owens, CakeML: A verified implementation of ML, in: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, P.Sewell, ed., ACM Press, 2014, pp. 179–191. doi:10.1145/2535838.2535841.
G.Reger, N.Bjørner, M.Suda and A.Voronkov, AVATAR modulo theories, in: Proceedings of the 2nd Global Conference on Artificial Intelligence, C.Benzmüller, G.Sutcliffe and R.Rojas, eds, EPiC Series in Computing, Vol. 41, EasyChair Publications, 2016, pp. 39–52.
12.
G.Reger, M.Suda and A.Voronkov, Finding finite models in multi-sorted first order logic, in: Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing, N.Creignou and D.Le Berre, eds, Lecture Notes in Computer Science, Springer-Verlag, 2016.
13.
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.
14.
A.Steen, M.Wisniewski and C.Benzmüller, Agent-based HOL reasoning, in: Proceedings of the 5th International Congress on Mathematical Software, G.-M.Greuel, T.Koch, P.Paule and A.Sommese, eds, Lecture Notes in Computer Science, Vol. 9725, Springer-Verlag, 2016, pp. 75–81.
15.
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.
16.
G.Sutcliffe, The CADE-16 ATP system competition, Journal of Automated Reasoning24(3) (2000), 371–396. doi:10.1023/A:1006393501098.
17.
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.
18.
G.Sutcliffe, in: Proceedings of the 8th IJCAR ATP System Competition, Coimbra, Portugal, 2016, http://www.tptp.org/CASC/J8/Proceedings.pdf.
19.
G.Sutcliffe, The CADE ATP system competition – CASC, AI Magazine37(2) (2016), 99–101.
20.
G.Sutcliffe and S.Schulz, The thousands of models for theorem provers (TMTP) model library – First steps, in: Proceedings of the 11th International Workshop on the Implementation of Logics, B.Konev, S.Schulz and L.Simon, eds, EPiC Series in Computing, Vol. 40, EasyChair Publications, 2016, pp. 106–121.
21.
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.
22.
G.Sutcliffe and J.Urban, The CADE-25 automated theorem proving system competition – CASC-25, AI Communications29(3) (2016), 423–433. doi:10.3233/AIC-150691.
23.
R.Veroff, Using hints to increase the effectiveness of an automated reasoning program: Case studies, Journal of Automated Reasoning16(3) (1996), 223–239. doi:10.1007/BF00252178.
24.
M.Wisniewski, A.Steen and C.Benzmüller, LeoPARD – A generic platform for the implementation of higher-order reasoners, in: Proceedings of the International Conference on Intelligent Computer Mathematics, M.Kerber, J.Carette, C.Kaliszyk, F.Rabe and V.Sorge, eds, Lecture Notes in Computer Science, Vol. 9150, Springer-Verlag, 2015, pp. 325–330.
25.
M.Wisniewski, A.Steen, K.Kern and C.Benzmüller, Effective normalization techniques for HOL, in: Proceedings of the 8th International Joint Conference on Automated Reasoning, N.Olivetti and A.Tiwari, eds, Lecture Notes in Artificial Intelligence, Vol. 9706, 2016, pp. 362–370.
