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-27 was the twenty-fourth competition in the CASC series. Twenty-five 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

Alama ,

Heskes ,

Külwein ,

Tsivtsivadze and

Urban , Premise selection for mathematics by corpus analysis and kernel methods, Journal of Automated Reasoning 52(2) (2014), 191–213. doi:10.1007/s10817-013-9286-5.

Barbosa ,

Reynolds ,

El Ouraoui ,

Tinelli and

Barrett , Extending SMT solvers to higher-order logic, in: Proceedings of the 27th International Conference on Automated Deduction,

Fontaine , ed., Lecture Notes in Computer Science, Vol. 11716, Springer-Verlag, 2019, pp. 35–54.

Barrett ,

Conway ,

Deters ,

Hadarean ,

Jovanovic ,

King ,

Reynolds and

Tinelli , CVC4, in: Proceedings of the 23rd International Conference on Computer Aided Verification,

Gopalakrishnan and

Qadeer , eds, Lecture Notes in Computer Science, Vol. 6806, Springer-Verlag, 2011, pp. 171–177. doi:10.1007/978-3-642-22110-1_14.

Bartocci ,

Beyer ,

P.E.

Black ,

Fedyukovich ,

Garavel ,

Hartmanns ,

Huisman ,

Kordon ,

Nagele ,

Sighireanu ,

Steffen ,

Suda ,

Sutcliffe ,

Weber and

Tamada , TOOLympics 2019: An overview of competitions in formal methods, in: Proceedings of the 2019 International Conference on Tools and Algorithms for the Construction and Analysis of Systems,

Vojnar and

Zhang , eds, Lecture Notes in Computer Science, Vol. 11429, Springer-Verlag, 2019, page to appear.

Bhayat and

Reger , Set of support for higher-order reasoning, in: Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning, Number 2162 in CEUR Workshop Proceedings,

Konev ,

Rümmer and

Urban , eds, 2018, pp. 2–16.

Bhayat and

Reger , Restricted combinatory unification, in: Proceedings of the 27th International Conference on Automated Deduction,

Fontaine , ed., Lecture Notes in Computer Science, Vol. 11716, Springer-Verlag, 2019, pp. 74–93.

Brown ,

Gauthier ,

Kaliszyk ,

Sutcliffe and

Urban , GRUNGE: A grand unified ATP challenge, in: Proceedings of the 27th International Conference on Automated Deduction,

Fontaine , ed., Lecture Notes in Computer Science, Vol. 11716, Springer-Verlag, 2019, pp. 123–141.

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.

Claessen and

Sörensson , New techniques that improve MACE-style finite model finding, in: Proceedings of the CADE-19 Workshop: Model Computation – Principles, Algorithms, Applications,

Baumgartner and

Fermueller , eds, 2003.

10.

Cruanes , Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond, PhD thesis, Ecole Polytechnique, Paris, France, 2015.

11.

Gauthier and

Kaliszyk , Premise selection and external provers for HOL4, in: Proceedings of the 4th ACM SIGPLAN Conference on Certified Programs and Proofs,

Leroy and

Tiu , eds, ACM Press, 2015, pp. 49–57.

12.

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-Verlag, 2011, pp. 299–314.

13.

Jakubuv and

Urban , Enhancing ENIGMA given clause guidance, in: Proceedings of the 11th International Conference on Intelligent Computer Mathematics,

Rabe ,

Farmer ,

Passmore and

Youssef , eds, Lecture Notes in Artificial Intelligence, Vol. 11006, Springer-Verlag, 2018, pp. 118–124. doi:10.1007/978-3-319-96812-4_11.

14.

Jakubuv and

Urban , Hammering mizar by learning clause guidance, in: Proceedings of the 10th International Conference on Interactive Theorem Proving, Leibniz International Proceedings in Informatics, Dagstuhl Publishing, 2019, page to appear.

15.

Jensen and

Pietrzykowski , Mechanizing omega-order type theory through unification, Theoretical Computer Science 3(2) (1976), 123–171. doi:10.1016/0304-3975(76)90021-9.

16.

Kotelnikov ,

Kovacs ,

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, 2016, pp. 37–48.

17.

Külwein ,

van Laarhoven ,

Tsivtsivadze ,

Urban and

Heskes , Overview and evaluation of premise selection techniques for large theory mathematics, 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. 378–392.

18.

Nieuwenhuis ,

Oliveras and

Tinelli , Solving SAT and SAT modulo theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T), Journal of the ACM 53(6) (2006), 937–977. doi:10.1145/1217856.1217859.

19.

Rawson and

Reger , Dynamic strategy priority: Empower the strong and abandon the weak, in: Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning, Number 2162 in CEUR Workshop Proceedings,

Konev ,

Rümmer and

Urban , eds, 2018, pp. 58–71.

20.

Rawson and

Reger , Old or heavy? Decaying gracefully with age/weight shapes, in: Proceedings of the 27th International Conference on Automated Deduction,

Fontaine , ed., Lecture Notes in Computer Science, Vol. 11716, Springer-Verlag, 2019, pp. 462–476.

21.

Reger ,

Reiner and

Suda , Symmetry avoidance in MACE-style finite model finding, in: Proceedings of the 12th International Conference on Frontiers of Combining Systems,

Herzig and

Popescu , eds, Lecture Notes in Computer Science, Vol. 11715, Springer-Verlag, 2019, pp. 3–21. doi:10.1007/978-3-030-29007-8_1.

22.

Reynolds ,

Tinelli ,

Jovanovic and

Barrett , Designing theory solvers with extensions, in: Proceedings of the 11th International Symposium on Frontiers of Combining Systems,

Dixon and

Finger , eds, Lecture Notes in Computer Science, Vol. 10483, Springer-Verlag, 2017, pp. 22–40. doi:10.1007/978-3-319-66167-4_2.

23.

Schulz ,

Cruanes and

Vukmirovic , Faster, higher, stronger: E 2.3, in: Proceedings of the 27th International Conference on Automated Deduction,

Fontaine , ed., Lecture Notes in Computer Science, Vol. 11716, Springer-Verlag, 2019, pp. 495–507.

24.

Schulz and

Möhrmann , Performance of clause selection heuristics for saturation-based theorem proving, in: Proceedings of the 8th International Joint Conference on Automated Reasoning,

Olivetti and

Tiwari , eds, Lecture Notes in Artificial Intelligence, Vol. 9706, 2016, pp. 330–345.

25.

Slind and

Norrish , A brief overview of HOL4, in: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics,

Mohamed ,

Munoz and

Tahar , eds, Lecture Notes in Computer Science, Vol. 5170, Springer-Verlag, 2008, pp. 28–32. doi:10.1007/978-3-540-71067-7_6.

26.

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

27.

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.

28.

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

29.

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, Number 418 in CEUR Workshop Proceedings,

Sutcliffe ,

Rudnicki ,

Schmidt ,

Konev and

Schulz , eds, 2008, pp. 38–49.

30.

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.

31.

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

32.

Sutcliffe , The 9th IJCAR automated theorem proving system competition – CASC-J9, AI Communications 31(6) (2018), 495–507. doi:10.3233/AIC-180773.

33.

Sutcliffe , Proceedings of the CADE-27 ATP System Competition. Natal, Brazil, 2019. http://www.tptp.org/CASC/27/Proceedings.pdf.

34.

Sutcliffe ,

Schulz ,

Claessen and

Van Gelder , Using the TPTP language for writing derivations and finite interpretations, in: Proceedings of the 3rd International Joint Conference on Automated Reasoning,

Furbach and

Shankar , eds, Lecture Notes in Artificial Intelligence, Vol. 4130, 2006, pp. 67–81.

35.

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-27 Automated theorem proving System Competition – CASC-27

Abstract

Keywords

Get full access to this article

References