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-28 was the twenty-sixth competition in the CASC series. Twenty-two ATP systems 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

P.B.

Andrews,

Bishop,

Issar,

Nesmith,

Pfenning and

Xi, TPS: A theorem-proving system for classical type theory, Journal of Automated Reasoning 16(3) (1996), 321–353. doi:10.1007/BF00252180.

P.B.

Andrews and

C.E.

Brown, TPS: A hybrid automatic-interactive system for developing proofs, Journal of Applied Logic 4(4) (2006), 367–395. doi:10.1016/j.jal.2005.10.002.

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.

Bentkamp,

Blanchette,

Cruanes and

Waldmann, Superposition for lambda-free higher-order logic, Logical Methods in Computer Science 17(2) (2021), Online.

Bentkamp,

Blanchette,

Tourret and

Vukmirović, Superposition for full higher-order logic, in: Proceedings of the 28th International Conference on Automated Deduction,

Platzer and

Sutcliffe, eds, Lecture Notes in Computer Science, Springer-Verlag, 2021, pp. 396–412.

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, 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, 2012, pp. 111–117.

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, 2018, pp. 388–404.

de Moura and

Bjørner, Z3: An efficient SMT solver, in: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems,

Ramakrishnan and

Rehof, eds, Lecture Notes in Artificial Intelligence, Springer-Verlag, 2008, pp. 337–340.

10.

Duarte and

Korovin, Implementing superposition in iProver, in: Proceedings of the 10th International Joint Conference on Automated Reasoning,

Peltier and

Sofronie-Stokkermans, eds, Lecture Notes in Artificial Intelligence, 2020, pp. 388–397.

11.

Duarte and

Korovin, AC simplifications and closure redundancies in the superposition calculus, in: Proceedings of the 30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods,

Das and

Negri, eds, Lecture Notes in Artificial Intelligence, Springer-Verlag, 2021, pp. 200–217. doi:10.1007/978-3-030-86059-2_12.

12.

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, Springer-Verlag, 2004, pp. 502–518. doi:10.1007/978-3-540-24605-3_37.

13.

Hernandez and

Korovin, An abstraction-refinement framework for reasoning with large theories, in: Proceedings of the 9th International Joint Conference on Automated Reasoning,

Galmiche,

Schulz and

Sebastiani, eds, Lecture Notes in Computer Science, 2018, pp. 663–679.

14.

Hillenbrand,

Jaeger and

Löchner, Waldmeister – improvements in performance and ease of use, in: Proceedings of the 16th International Conference on Automated Deduction,

Ganzinger, ed., Lecture Notes in Artificial Intelligence, Springer-Verlag, 1999, pp. 232–236. doi:10.1007/3-540-48660-7_20.

15.

Holden and

Korovin, SMAC and XGBoost your theorem prover, in: Proceedings of the 4th Conference on Artificial Intelligence and Theorem Proving,

Hales,

Kaliszyk,

Kumar,

Schulz and

Urban, eds, 2019, pp. 93–95.

16.

Holden and

Korovin, Heterogeneous heuristic optimisation and scheduling for first-order theorem proving, in: Proceedings of the 14th International Conference on Intelligent Computer Mathematics,

Kamareddine and

Sacerdoti, eds, Lecture Notes in Computer Science, Springer-Verlag, 2021, pp. 107–123. doi:10.1007/978-3-030-81097-9_8.

17.

Korovin, iProver – an instantiation-based theorem prover for first-order logic (system description), in: Proceedings of the 4th International Joint Conference on Automated Reasoning,

Baumgartner,

Armando and

Dowek, eds, Lecture Notes in Artificial Intelligence, 2008, pp. 292–298.

18.

Korovin, Inst-Gen – a modular approach to instantiation-based automated reasoning, in: Programming Logics, Essays in Memory of Harald Ganzinger,

Voronkov and

Weidenbach, eds, Lecture Notes in Computer Science, Springer-Verlag, 2013, pp. 239–270. doi:10.1007/978-3-642-37651-1_10.

19.

Kotelnikov,

Kovacs,

Suda and

Voronkov, A clausal normal form translation for FOOL, in: Proceedings of the 2nd Global Conference on Artificial Intelligence,

Benzmüller,

Sutcliffe and

Rojas, eds, EPiC Series in Computing, EasyChair Publications, 2016, pp. 53–71.

20.

Kovacs and

Voronkov, First-order theorem proving and vampire, in: Proceedings of the 25th International Conference on Computer Aided Verification,

Sharygina and

Veith, eds, Lecture Notes in Artificial Intelligence, Springer-Verlag, 2013, pp. 1–35.

21.

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, Springer-Verlag, 1990, pp. 366–380. doi:10.1007/3-540-52885-7_100.

22.

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, EasyChair Publications, 2010, pp. 1–11.

23.

Schlichtkrull,

Blanchette and

Traytel, A verified prover based on ordered resolution, in: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs,

Mahboubi and

Myreen, eds, ACM Press, 2019, pp. 152–165. doi:10.1145/3293880.3294100.

24.

Schlichtkrull,

Blanchette,

Traytel and

Waldmann, Formalizing Bachmair and Ganzinger’s ordered resolution prover, Journal of Automated Reasoning 64(7) (2020), 1169–1195. doi:10.1007/s10817-020-09561-0.

25.

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

McCune,

M.P.

Bonacina and

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

26.

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, Springer-Verlag, 2019, pp. 495–507.

27.

Smallbone, Twee: An equational theorem prover (system description), in: Proceedings of the 28th International Conference on Automated Deduction,

Platzer and

Sutcliffe, eds, Lecture Notes in Computer Science, Springer-Verlag, 2021, pp. 602–613.

28.

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, 2014, pp. 367–373.

29.

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

30.

Sutcliffe, The 7th IJCAR automated theorem proving system competition – CASC-J7, AI Communications 28(4) (2015), 683–692. doi:10.3233/AIC-150668.

31.

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

32.

Sutcliffe, The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0, Journal of Automated Reasoning 59(4) (2017), 483–502. doi:10.1007/s10817-017-9407-7.

33.

Sutcliffe, The CADE-27 automated theorem proving system competition – CASC-27, AI Communications 32(5–6) (2020), 373–389. doi:10.3233/AIC-190627.

34.

Sutcliffe, The 10th IJCAR automated theorem proving system competition – CASC-J10, AI Communications 34(2) (2021), 164–177. doi:10.3233/AIC-201566.

35.

Sutcliffe, Proceedings of the CADE-28 ATP System Competition, Online, 2021, http://www.tptp.org/CASC/28/Proceedings.pdf.

36.

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.

37.

Sutcliffe,

Zimmer and

Schulz, TSTP data-exchange formats for automated theorem proving tools, in: Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems,

Zhang and

Sorge, eds, Frontiers in Artificial Intelligence and Applications, IOS Press, 2004, pp. 201–215.

38.

Vukmirović,

Bentkamp,

Blanchette,

Cruanes,

Nummelin and

Tourret, Making higher-order superposition work, in: Proceedings of the 28th International Conference on Automated Deduction,

Platzer and

Sutcliffe, eds, Lecture Notes in Computer Science, Springer-Verlag, 2021, pp. 415–432.

39.

Vukmirovic,

Blanchette,

Cruanes and

Schulz, Extending a brainiac prover to lambda-free higher-order logic, in: Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems,

Vojnar and

Zhang, eds, Lecture Notes in Computer Science, Springer-Verlag, 2019, pp. 192–210.

The CADE-28 Automated Theorem Proving System Competition – CASC-28

Abstract

Keywords

Get full access to this article

References