The CADE ATP System Competition (CASC) is an annual evaluation of fully automatic, classical logic Automated Theorem Proving (ATP) systems. CASC-25 was the twentieth competition in the CASC series. Twenty-seven 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.
P.Backeman and P.Rümmer, Efficient algorithms for bounded rigid E-unification, in: Proceedings of the 24th Conference on Automated Reasoning with Analytic Tableaux and Related Methods, H.de Nivelle, ed., Lecture Notes in Computer Science, Vol. 9323, Springer-Verlag, 2015, pp. 70–85.
2.
P.Backeman and P.Rümmer, Theorem proving with bounded rigid E-unification, in: Proceedings of the 25th International Conference on Automated Deduction, A.Felty and A.Middeldorp, eds, Lecture Notes in Computer Science, Vol. 9195, Springer-Verlag, 2015, pp. 572–587.
3.
R.Bonichon, D.Delahaye and D.Doligez, Zenon: An extensible automated theorem prover producing checkable proofs, in: Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, N.Dershowitz and A.Voronkov, eds, Lecture Notes in Artificial Intelligence, Vol. 4790, 2007, pp. 151–165.
4.
G.Bury and D.Delahaye, Integrating simplex with tableaux, in: Proceedings of the 24th Conference on Automated Reasoning with Analytic Tableaux and Related Methods, H.de Nivelle, ed., Lecture Notes in Computer Science, Vol. 9323, Springer-Verlag, 2015, pp. 86–101.
5.
L.de Moura and N.Bjorner, Z3: An efficient SMT solver, in: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, C.Ramakrishnan and J.Rehof, eds, Lecture Notes in Artificial Intelligence, Vol. 4963, Springer-Verlag, 2008, pp. 337–340.
6.
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.
7.
A.Reynolds, M.Deters, V.Kuncak, C.Barrett and C.Tinelli, Counterexample guided quantifier instantiation for synthesis in CVC4, in: Proceedings of the 27th International Conference on Computer Aided Verification, D.Kroening and C.Pasareanu, eds, Lecture Notes in Computer Science, Vol. 9207, Springer-Verlag, 2015, pp. 198–216.
8.
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, Vol. 5330, Springer-Verlag, 2008, pp. 274–289.
9.
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.
10.
G.Sutcliffe, The CADE-16 ATP system competition, Journal of Automated Reasoning24(3) (2000), 371–396.
11.
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.
12.
G.Sutcliffe, The TPTP World – Infrastructure for automated reasoning, in: Proceedings of the 16th International Conference on Logic for Programming Artificial Intelligence and Reasoning, E.Clarke and A.Voronkov, eds, Lecture Notes in Artificial Intelligence, Vol. 6355, Springer-Verlag, 2010, pp. 1–12.
13.
G.Sutcliffe, in: Proceedings of the CADE-25 ATP System Competition, Berlin, Germany, 2015, http://www.tptp.org/CASC/25/Proceedings.pdf.
14.
G.Sutcliffe, The 7th IJCAR Automated Theorem Proving system competition – CASC-J7, AI Communications28(4) (2015), 683–692.
15.
G.Sutcliffe and C.B.Suttner, Evaluating general purpose automated theorem proving systems, Artificial Intelligence131(1,2) (2001), 39–54.
16.
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, Vol. 8559, 2014, pp. 696–710.
17.
M.Wisniewski, A.Steen and C.Benzmüller, The Leo-III project, in: Proceedings of the Joint Automated Reasoning Workshop and Deduktionstreffen, A.Bolotov and M.Kerber, eds, 2014, p. 38.
