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-26 was the twenty-second 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.

Keywords

Automated theorem proving competition

Get full access to this article

View all access options for this article.

References

Backes and

C.E.

Brown, Analytic tableaux for higher-order logic with choice, Journal of Automated Reasoning 47(4) (2011), 451–479. doi:10.1007/s10817-011-9233-2.

Becker,

Blanchette,

Waldmann and

Wand, A transfinite Knuth–Bendix order for lambda-free higher-order terms, in: Proceedings of the 26th International Conference on Automated Deduction (CADE 2017),

de Moura, ed., Lecture Notes in Computer Science, Vol. 10395, Springer, Cham, 2017, pp. 432–453. doi:10.1007/978-3-319-63046-5_27.

Beeson and

Wos, Finding proofs in tarskian geometry, Journal of Automated Reasoning 58(1) (2017), 181–217. doi:10.1007/s10817-016-9392-2.

Benzmüller,

Steen and

Wisniewski, Leo-III version 1.1 (system description), in: Proceedings of the IWIL Workshop and LPAR Short Presentations,

Eiter,

Sands,

Schulz,

Urban,

Sutcliffe and

Voronkov, eds, Kalpa Publications in Computing, Vol. 1, 2017.

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 (ARCADE 2017),

Reger and

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

C.E.

Brown, Satallax: An automated higher-order prover (system description), in: Proceedings of the 6th International Joint Conference on Automated Reasoning,

Gramlich,

Miller and

Sattler, eds, Lecture Notes in Artificial Intelligence, Vol. 7364, 2012, pp. 111–117.

C.E.

Brown, Reducing higher-order theorem proving to a sequence of SAT problems, Journal of Automated Reasoning 51(1) (2013), 57–77. doi:10.1007/s10817-013-9283-8.

C.E.

Brown and

Smolka, Analytic tableaux for simple type theory and its first-order fragment, Logical Methods in Computer Science 6(2) (2010), 1–33. doi:10.2168/LMCS-6(2:3)2010.

Cruanes, Extending superposition with integer arithmetic, structural induction, and beyond, PhD thesis, Ecole Polytechnique, Paris, France, 2015.

10.

Dowek,

Hardin and

Kirchner, Theorem proving modulo, Journal of Automated Reasoning 31(1) (2003), 33–72. doi:10.1023/A:1027357912519.

11.

Eén and

Sörensson, An extensible SAT-solver, in: Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing,

Giunchiglia and

Tacchella, eds, Lecture Notes in Computer Science, Vol. 2919, Springer, Berlin, 2004, pp. 502–518. doi:10.1007/978-3-540-24605-3_37.

12.

Hales, A revision of the proof of the Kepler conjecture, Discrete and Computational Geometry 44(1) (2010), 1–34. doi:10.1007/s00454-009-9148-4.

13.

Hoder and

Voronkov, Sine qua non for large theory reasoning, in: Proceedings of the 23rd International Conference on Automated Deduction,

Sofronie-Stokkermans and

Bjœrner, eds, Lecture Notes in Artificial Intelligence, Vol. 6803, Springer, Berlin, 2011, pp. 299–314. doi:10.1007/978-3-642-22438-6_23.

14.

Kaliszyk,

Chollet and

Szegedy, HolStep: A machine learning dataset for higher-order logic theorem proving, in: Proceedings of the 6th International Conference on Learning Representations (ICRL 2017),

Murray,

Ranzato and

Vinyals, eds, 2018, to appear.

15.

Kaliszyk and

Rabe, Towards knowledge management for HOL light, in: Proceedings of the International Conference on Intelligent Computer Mathematics,

Watt,

Davenport,

Sexton,

Sojka and

Urban, eds, Lecture Notes in Computer Science, Vol. 8543, Springer, Cham, 2014, pp. 357–372. doi:10.1007/978-3-319-08434-3_26.

16.

Kotelnikov,

Kovacsi,

Reger and

Voronkov, The Vampire and the FOOL, in: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs,

Avigad and

Chlipala, eds, ACM, New York, 2016, pp. 37–48.

17.

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.

18.

Miller, A logic programming language with lambda-abstraction, function variables, and simple unification, Journal of Logic and Computation 1(4) (1991), 497–536. doi:10.1093/logcom/1.4.497.

19.

Paulson and

Blanchette, Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers, in: Proceedings of the 8th International Workshop on the Implementation of Logics,

Sutcliffe,

Ternovska and

Schulz, eds, EPiC Series in Computing, Vol. 2, 2010, pp. 1–11.

20.

Reger,

Suda and

Voronkov, New techniques in clausal form generation, in: Proceedings of the 2nd Global Conference on Artificial Intelligence,

Benzmüller,

Sutcliffe and

Rojas, eds, EPiC Series in Computing, Vol. 41, EasyChair Publications, 2016, pp. 11–23.

21.

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, Berlin, 2013, pp. 45–67. doi:10.1007/978-3-642-36675-8_3.

22.

Steen,

Wisniewski and

Benzmüller, Agent-based HOL reasoning, in: Proceedings of the 5th International Congress on Mathematical Software (ICMS 2016),

G.-M.

Greuel,

Koch,

Paule and

Sommese, eds, Lecture Notes in Computer Science, Vol. 9725, Springer, Cham, 2016, pp. 75–81. doi:10.1007/978-3-319-42432-3_10.

23.

Steen,

Wisniewski and

Benzmüller, Agent-based HOL reasoning, in: Proceedings of the IWIL Workshop and LPAR Short Presentations,

Eiter,

Sands,

Sutcliffe and

Voronkov, eds, Kalpa Publications in Computing, Vol. 1, 2016.

24.

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.

25.

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

26.

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.

27.

Sutcliffe, The TPTP world – infrastructure for automated reasoning, in: Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning,

Clarke and

Voronkov, eds, Lecture Notes in Artificial Intelligence, Vol. 6355, Springer, Berlin, 2010, pp. 1–12. doi:10.1007/978-3-642-17511-4_1.

28.

Sutcliffe, Proceedings of the 8th IJCAR ATP System Competition (CASC-J8), Coimbra, Portugal, 2016, http://www.tptp.org/CASC/J8/Proceedings.pdf.

29.

Sutcliffe, The 8th IJCAR automated theorem proving system competition – CASC-J8, AI Communications 29(5) (2016), 607–619. doi:10.3233/AIC-160709.

30.

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

31.

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.

The CADE-26 automated theorem proving system competition – CASC-26

Abstract

Keywords

Get full access to this article

References