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-J11 was the twenty-seventh competition in the CASC series. Twenty-four 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

Ammer and

Lammich, van Emde Boas trees, Archive of Formal Proofs (2021). http://isa-afp.org/entries/Van_Emde_Boas_Trees.html.

Baumgartner,

Bax and

Waldmann, Beagle – A hierarchic superposition theorem prover, in: Proceedings of the 25th International Conference on Automated Deduction,

Felty and

Middeldorp, eds, Lecture Notes in Computer Science, Springer-Verlag, 2015, pp. 285–294.

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.

Bentkamp,

Blanchette,

Tourret,

Vukmirović and

Waldmann, Superposition with lambdas, Journal of Automated Reasoning 65(7) (2021), 893–940. doi:10.1007/s10817-021-09595-y.

Blanchette and

Nipkow, Nitpick: A counterexample generator for higher-order logic based on a relational model finder, in: Proceedings of the 1st International Conference on Interactive Theorem Proving,

Kaufmann and

Paulson, eds, Lecture Notes in Computer Science, Springer-Verlag, 2010, pp. 131–146. doi:10.1007/978-3-642-14052-5_11.

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, Springer-Verlag, 2019, pp. 123–141.

Brown and

Kaliszyk, Lash 1.0 system description, in: Proceedings of the 11th International Joint Conference on Automated Reasoning,

Blanchette,

Kovacs and

Pattinson, eds, Lecture Notes in Artificial Intelligence, 2022, pp. 350–358. doi:10.1007/978-3-031-10769-6_21.

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. doi:10.1007/978-3-642-31365-3_11.

Cailler,

Rosain,

Delahaye,

Robillard and

Bouziane, Goéland: A concurrent tableau-based theorem prover, in: Proceedings of the 11th International Joint Conference on Automated Reasoning,

Blanchette,

Kovacs and

Pattinson, eds, Lecture Notes in Artificial Intelligence, 2022, pp. 359–368. doi:10.1007/978-3-031-10769-6_22.

10.

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. doi:10.1007/978-3-319-94205-6_26.

11.

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.

12.

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

13.

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.

14.

D’Silva,

Kroening and

Weissenbacher, A survey of automated techniques for formal software verification, IEEE Transactions on Computer-aided Design of Integrated Circuits and Systems 27(7) (2008), 1165–1178. doi:10.1109/TCAD.2008.923410.

15.

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. doi:10.1007/978-3-030-51054-1_24.

16.

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.

17.

Duarte and

Korovin, Ground joinability and connectedness in the superposition calculus, in: Proceedings of the 11th International Joint Conference on Automated Reasoning,

Blanchette,

Kovacs and

Pattinson, eds, Lecture Notes in Artificial Intelligence, 2022, pp. 169–187. doi:10.1007/978-3-031-10769-6_11.

18.

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.

19.

Fish and

Lisitsa, Detecting unknots via equational reasoning, I: Exploration, in: Proceedings of the 7th International Conference on Intelligent Computer Mathematics,

Watt,

Davenport,

Sexton,

Sojka and

Urban, eds, Lecture Notes in Artificial Intelligence, Springer-Verlag, 2014, pp. 76–91. doi:10.1007/978-3-319-08434-3_7.

20.

Galatos and

Tsinakis, Generalized MV-algebras, Journal of Algebra 283 (2005), 254–291. doi:10.1016/j.jalgebra.2004.07.002.

21.

Gleiss and

Suda, Layered clause selection for theory reasoning, in: Proceedings of the 10th International Joint Conference on Automated Reasoning,

Peltier and

Sofronie-Stokkermans, eds, Lecture Notes in Computer Science, 2020, pp. 402–409. doi:10.1007/978-3-030-51074-9_23.

22.

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. doi:10.1007/978-3-319-94205-6_43.

23.

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.

24.

Kaliszyk and

Urban, Automated reasoning service for HOL light, in: Proceddings of the International Conference on Intelligent Computer Mathematics,

Carette,

Aspinall,

Lange,

Sojka and

Windsteiger, eds, Lecture Notes in Computer Science, Springer-Verlag, 2013, pp. 120–135. doi:10.1007/978-3-642-39320-4_8.

25.

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. doi:10.1007/978-3-540-71070-7_24.

26.

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.

27.

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.

28.

Litak,

Mikulás and

Hidders, Relational lattices: From databases to universal algebra, Journal of Logical and Algebraic Methods in Programming 85(4) (2016), 540–573. doi:10.1016/j.jlamp.2015.11.008.

29.

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.

30.

Prevosto and

Waldmann, SPASS+T, in: Proceedings of the FLoC’06 Workshop on Empirically Successful Computerized Reasoning, 3rd International Joint Conference on Automated Reasoning,

Sutcliffe,

Schmidt and

Schulz, eds, CEUR Workshop Proceedings, 2006, pp. 19–33.

31.

Reger,

Schoisswohl and

Voronkov, Making theory reasoning simpler, in: Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems,

Groote and

Larsen, eds, Lecture Notes in Computer Science, Springer-Verlag, 2021, pp. 164–180.

32.

Reger,

Suda and

Voronkov, Playing with AVATAR, in: Proceedings of the 25th International Conference on Automated Deduction,

Felty and

Middeldorp, eds, Lecture Notes in Computer Science, Springer-Verlag, 2015, pp. 399–415.

33.

Robinson and

Voronkov, Handbook of Automated Reasoning, Elsevier Science, 2001.

34.

Roussel, Controlling a solver execution with the runsolver tool, Journal of Satisfiability, Boolean Modeling and Computation 7(4) (2011), 139–144. doi:10.3233/SAT190083.

35.

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,

Cervesato,

Veith and

Voronkov, eds, Lecture Notes in Artificial Intelligence, Springer-Verlag, 2008, pp. 274–289.

36.

Schulz, Empirical properties of term orderings for superposition, in: Proceedings of the 8th Workshop on Practical Aspects of Automated Reasoning,

Konev,

Schon and

Steen, eds, CEUR Workshop Proceedings, 2022, Online.

37.

Schulz,

Cruanes and

Vukmirović, 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.

38.

Schulz,

Sutcliffe,

Urban and

Pease, Detecting inconsistencies in large first-order knowledge bases, in: Proceedings of the 26th International Conference on Automated Deduction,

de Moura, ed., Lecture Notes in Computer Science, Springer-Verlag, 2017, pp. 310–325.

39.

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. doi:10.1007/978-3-319-08587-6_28.

40.

Suda, Vampire getting noisy: Will random bits help conquer chaos? (system description), EasyChair Preprint no. 7719, 2022.

41.

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

42.

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

43.

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.

44.

Sutcliffe, Proceedings of the 11th IJCAR ATP System Competition, Online, 2021. http://www.tptp.org/CASC/J11/Proceedings.pdf.

45.

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

46.

Sutcliffe, The logic languages of the TPTP world, Logic Journal of the IGPL (2022). doi:10.1093/jigpal/jzac068.

47.

Sutcliffe and

Desharnais, The CADE-28 automated theorem proving system competition – CASC-28, AI Communications 34(4) (2022), 259–276. doi:10.3233/AIC-210235.

48.

Sutcliffe and

C.B.

Suttner, Evaluating general purpose automated theorem proving systems, Artificial Intelligence 131(1–2) (2001), 39–54.

49.

Urban and

Sutcliffe, ATP-based cross verification of Mizar proofs: Method, systems, and first experiments, Journal of Mathematics in Computer Science 2(2) (2009), 231–251.

50.

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.

51.

Vukmirović,

Bentkamp and

Nummelin, Efficient full higher-order unification, in: Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction,

Z.M.

Ariola, ed., Leibniz International Proceedings in Informatics, Dagstuhl Publishing, 2020, pp. 5:1–5:20.

52.

Vukmirović,

Blanchette,

Cruanes and

Schulz, Extending a brainiac prover to lambda-free higher-order logic, International Journal on Software Tools for Technology Transfer 24 (2021), 67–87. doi:10.1007/s10009-021-00639-7.

53.

Vukmirović and

Nummelin, Boolean reasoning in a higher-order superposition prover, in: Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning,

Fontaine,

Rümmer and

Tourret, eds, CEUR Workshop Proceedings, 2020, pp. 148–166.

54.

Winker, Generation and verification of finite models and counterexamples using an automated theorem prover answering two open questions, Journal of the ACM 29(2) (1982), 273–284. doi:10.1145/322307.322308.

The 11th IJCAR automated theorem proving system competition – CASC-J11

Abstract

Keywords

Get full access to this article

References