Sage Journals: Discover world-class research

Abstract

The CADE ATP System Competition (CASC) is the annual evaluation of fully automatic, classical logic Automated Theorem Proving (ATP) systems. CASC-J9 was the twenty-third competition in the CASC series. Twenty-three 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.

Keywords

Automated theorem proving competition

Get full access to this article

View all access options for this article.

References

Bachmair and

Dershowitz, Critical pair criteria for completion, Journal of Symbolic Computation 6(1) (1988), 1–18. doi:10.1016/S0747-7171(88)80018-X.

Blanchette,

Fontaine,

Schulz and

Waldmann, Towards strong higher-order automation for fast interactive verification, in: Proceedings of the 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements,

Reger and

Trayfel, eds, EPiC Series in Computing, Vol. 51, EasyChair Publications, 2017, pp. 16–23.

Claessen and

Smallbone, Efficient encodings of first-order Horn formulas in equational logic, in: Proceedings of the 9th International Joint Conference on Automated Reasoning,

Galmiche,

Schulz and

Sebastiani, eds, Lecture Notes in Computer Science, Vol. 10900, 2018, pp. 388–404.

Hoder,

Reger,

Suda and

Voronkov, Selecting the selection, in: Proceedings of the 8th International Joint Conference on Automated Reasoning,

Olivetti and

Tiwari, eds, Lecture Notes in Artificial Intelligence, Vol. 9706, 2016, pp. 313–329.

Kiesl,

Suda,

Seidl,

Tompits and

Biere, Blocked clauses in first-order logic, in: Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence, and Reasoning,

Eiter and

Sands, eds, EPiC Series in Computing, Vol. 46, EasyChair Publications, 2017, pp. 31–48.

Kumar,

Myreen,

Norrish and

Owens, CakeML: A verified implementation of ML, in: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,

Sewell, ed., ACM Press, 2014, pp. 179–191. doi:10.1145/2535838.2535841.

Martin and

Nipkow, Ordered rewriting and confluence, in: Proceedings of the 10th International Conference on Automated Deduction,

M.E.

Stickel, ed., Lecture Notes in Artificial Intelligence, Vol. 449, Springer-Verlag, 1990, pp. 366–380. doi:10.1007/3-540-52885-7_100.

Otten, A non-clausal connection calculus, in: Proceedings of the 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods,

Brünnler and

Metcalfe, eds, Lecture Notes in Artificial Intelligence, Vol. 6793, Springer-Verlag, 2011, pp. 226–241. doi:10.1007/978-3-642-22119-4_18.

Otten, nanoCoP: A non-clausal connection prover, in: Proceedings of the 7th International Joint Conference on Automated Reasoning,

Demri,

Kapur and

Weidenbach, eds, Lecture Notes in Artificial Intelligence, Vol. 8562, 2016, pp. 302–312.

10.

Otten, Non-clausal connection calculi for non-classical logics, in: Proceedings of the 26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods,

Nalon and

Schmidt, eds, Lecture Notes in Artificial Intelligence, Vol. 10501, Springer-Verlag, 2017, pp. 209–227. doi:10.1007/978-3-319-66902-1_13.

11.

Otten, Proof search optimizations for non-clausal connection calculi, in: Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning,

Konev,

Rümmer and

Urban, eds, CEUR Workshop Proceedings, Vol. 2162, 2018, pp. 49–57.

12.

Reger and

Suda, Set of support for theory reasoning, in: Proceedings of the IWIL Workshop and LPAR Short Presentations,

Eiter,

Sands,

Sutcliffe and

Voronkov, eds, Kalpa Publications in Computing, Vol. 1, 2017, pp. 124–134.

13.

Reger,

Suda and

Voronkov, Unification with abstraction and theory instantiation in saturation-based reasoning, in: Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems,

Beyer and

Huisman, eds, Lecture Notes in Computer Science, Vol. 10805, Springer-Verlag, 2018, pp. 3–22.

14.

Schulz, Simple and efficient clause subsumption with feature vector indexing, in: Automated Reasoning and Mathematics: Essays in Memory of William W. McCune,

M.P.

Bonacina and

Stickel, eds, Lecture Notes in Artificial Intelligence, Vol. 7788, Springer-Verlag, 2013, pp. 45–67. doi:10.1007/978-3-642-36675-8_3.

15.

Smith, An Introduction to Goedel’s Theorems, Cambridge University Press, 2007.

16.

Stump,

Sutcliffe and

Tinelli, StarExec: A cross-community infrastructure for logic solving, in: Proceedings of the 7th International Joint Conference on Automated Reasoning,

Demri,

Kapur and

Weidenbach, eds, Lecture Notes in Artificial Intelligence, Vol. 8562, 2014, pp. 367–373.

17.

Sutcliffe, The CADE-16 ATP system competition, Journal of Automated Reasoning 24(3) (2000), 371–396. doi:10.1023/A:1006393501098.

18.

Sutcliffe, The TPTP problem library and associated infrastructure. The FOF and CNF parts, v3.5.0, Journal of Automated Reasoning 43(4) (2009), 337–362. doi:10.1007/s10817-009-9143-8.

19.

Sutcliffe, The CADE ATP system competition – CASC, AI Magazine 37(2) (2016), 99–101. doi:10.1609/aimag.v37i2.2620.

20.

Sutcliffe, The CADE-26 Automated Theorem Proving System Competition – CASC-26, AI Communications 30(6) (2017), 419–432. doi:10.3233/AIC-170744.

21.

Sutcliffe, Proceedings of the 9th IJCAR ATP System Competition. Oxford, United Kingdom, 2018, http://www.tptp.org/CASC/J9/Proceedings.pdf.

22.

Sutcliffe and

C.B.

Suttner, Evaluating general purpose automated theorem proving systems, Artificial Intelligence 131(1–2) (2001), 39–54. doi:10.1016/S0004-3702(01)00113-8.

23.

Xu,

Liu,

Chen,

Zhong and

He, Contradiction separation based dynamic multi-clause synergized automated deduction, Information Sciences 462 (2018), 93–113. doi:10.1016/j.ins.2018.04.086.

The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9

Abstract

Keywords

Get full access to this article

References