The CADE ATP System Competition (CASC) is an annual evaluation of fully automatic, classical logic Automated Theorem Proving (ATP) systems. CASC-J7 was the nineteenth competition in the CASC series. Twenty-four ATP systems and system variants competed in the various competition and demonstration divisions. An outline of the competition design, and a commentated summary of the results, are presented.
C.Barrett, C.Conway, M.Deters, L.Hadarean, D.Jovanovic, T.King, A.Reynolds and C.Tinelli, CVC4, in: Proceedings of the 23rd International Conference on Computer Aided Verification, G.Gopalakrishnan and S.Qadeer, eds, Lecture Notes in Computer Science, Vol. 6806, Springer-Verlag, 2011, pp. 171–177.
2.
P.Baumgartner and U.Waldmann, Hierarchic superposition with weak abstraction, in: Proceedings of the 24th International Conference on Automated Deduction, M.P.Bonacina, ed., Lecture Notes in Artificial Intelligence, Vol. 7898, Springer-Verlag, 2013, pp. 39–57.
3.
A.Reynolds, C.Tinelli and L.de Moura, Finding conflicting instances of quantified formulas in SMT, in: Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design, K.Claessen and V.Kuncak, eds, 2014, pp. 195–202.
4.
A.Reynolds, C.Tinelli, A.Goel and S.Krstic, Finite model finding in SMT, in: Proceedings of the 25th International Conference on Computer Aided Verification, N.Sharygina and H.Veith, eds, Lecture Notes in Computer Science, Vol. 8044, Springer-Verlag, 2013, pp. 640–655.
5.
A.Reynolds, C.Tinelli, A.Goel, S.Krstic, M.Deters and C.Barrett, Quantifier instantiation techniques for finite model finding in SMT, in: Proceedings of the 24th International Conference on Automated Deduction, M.P.Bonacina, ed., Lecture Notes in Artificial Intelligence, Vol. 7898, Springer-Verlag, 2013, pp. 377–391.
6.
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.
7.
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.
8.
G.Sutcliffe, The CADE-16 ATP system competition, Journal of Automated Reasoning24(3) (2000), 371–396.
9.
G.Sutcliffe, The SZS ontologies for automated reasoning software, in: Proceedings of the LPAR Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, G.Sutcliffe, P.Rudnicki, R.Schmidt, B.Konev and S.Schulz, eds, CEUR Workshop Proceedings, Vol. 418, 2008, pp. 38–49.
10.
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.
11.
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.
12.
G.Sutcliffe, in: Proceedings of the 7th IJCAR ATP System Competition, Vienna, Austria, 2014.
13.
G.Sutcliffe, The CADE-24 automated theorem proving system competition – CASC-24, AI Communications27(4) (2014), 405–416.
14.
G.Sutcliffe and C.B.Suttner, Evaluating general purpose automated theorem proving systems, Artificial Intelligence131(1,2) (2001), 39–54.
15.
A.Voronkov, AVATAR: The new architecture for first-order theorem provers, in: Proceedings of Automated Reasoning, A.Biere and R.Bloem, eds, Lecture Notes in Computer Science, Vol. 8559, 2014, pp. 696–710.
