×

zbMATH — the first resource for mathematics

The 9th IJCAR automated theorem proving system competition – CASC-J9. (English) Zbl 1462.68220
Summary: 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.
MSC:
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] L. Bachmair and N. Dershowitz, Critical pair criteria for completion,Journal of Symbolic Computation6(1) (1988), 1-18. doi:10.1016/S0747-7171(88)80018-X. · Zbl 0651.68030
[2] J. Blanchette, P. Fontaine, S. Schulz and U. 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, G. Reger and D. Trayfel, eds, EPiC Series in Computing, Vol. 51, EasyChair Publications, 2017, pp. 16-23.
[3] K. Claessen and N. Smallbone, Efficient encodings of firstorder Horn formulas in equational logic, in:Proceedings of the 9th International Joint Conference on Automated Reasoning, D. Galmiche, S. Schulz and R. Sebastiani, eds, Lecture Notes in Computer Science, Vol. 10900, 2018, pp. 388-404. · Zbl 06958112
[4] K. Hoder, G. Reger, M. Suda and A. Voronkov, Selecting the selection, in:Proceedings of the 8th International Joint Conference on Automated Reasoning, N. Olivetti and A. Tiwari, eds, Lecture Notes in Artificial Intelligence, Vol. 9706, 2016, pp. 313-329. · Zbl 06623270
[5] B. Kiesl, M. Suda, M. Seidl, H. Tompits and A. Biere, Blocked clauses in first-order logic, in:Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, T. Eiter and D. Sands, eds, EPiC Series in Computing, Vol. 46, EasyChair Publications, 2017, pp. 31-48. · Zbl 1403.68240
[6] R. Kumar, M. Myreen, M. Norrish and S. Owens, CakeML: A verified implementation of ML, in:Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, P. Sewell, ed., ACM Press, 2014, pp. 179-191. doi:10.1145/2535838.2535841. · Zbl 1284.68405
[7] U. Martin and T. 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.
[8] J. Otten, A non-clausal connection calculus, in:Proceedings of the 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, K. Brünnler and G. Metcalfe, eds, Lecture Notes in Artificial Intelligence, Vol. 6793, Springer-Verlag, 2011, pp. 226-241. doi:10.1007/ 978-3-642-22119-4_18. · Zbl 1333.03004
[9] J. Otten, nanoCoP: A non-clausal connection prover, in:Proceedings of the 7th International Joint Conference on Automated Reasoning, S. Demri, D. Kapur and C. Weidenbach, eds, Lecture Notes in Artificial Intelligence, Vol. 8562, 2016, pp. 302-312.
[10] J. 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, C. Nalon and R. Schmidt, eds, Lecture Notes in Artificial Intelligence, Vol. 10501, Springer-Verlag, 2017, pp. 209- 227. doi:10.1007/978-3-319-66902-1_13. · Zbl 06833558
[11] J. Otten, Proof search optimizations for non-clausal connection calculi, in:Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning, B. Konev, P. Rümmer and J. Urban, eds, CEUR Workshop Proceedings, Vol. 2162, 2018, pp. 49-57.
[12] G. Reger and M. Suda, Set of support for theory reasoning, in: Proceedings of the IWIL Workshop and LPAR Short Presentations, T. Eiter, D. Sands, G. Sutcliffe and A. Voronkov, eds, Kalpa Publications in Computing, Vol. 1, 2017, pp. 124-134.
[13] G. Reger, M. Suda and A. 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, D. Beyer and M. Huisman, eds, Lecture Notes in Computer Science, Vol. 10805, Springer-Verlag, 2018, pp. 3-22. · Zbl 1423.68424
[14] S. 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 · Zbl 1383.68082
[15] P. Smith,An Introduction to Goedel’s Theorems, Cambridge University Press, 2007.
[16] A. Stump, G. Sutcliffe and C. Tinelli, StarExec: A crosscommunity infrastructure for logic solving, in:Proceedings of the 7th International Joint Conference on Automated Reasoning, S. Demri, D. Kapur and C. Weidenbach, eds, Lecture Notes in Artificial Intelligence, Vol. 8562, 2014, pp. 367-373.
[17] G. Sutcliffe, The CADE-16 ATP system competition,Journal of Automated Reasoning24(3) (2000), 371-396. doi:10.1023/ A:1006393501098. · Zbl 0953.68595
[18] G. Sutcliffe, The TPTP problem library and associated infrastructure. The FOF and CNF parts, v3.5.0,Journal of Automated Reasoning43(4) (2009), 337-362. doi:10.1007/s10817009-9143-8. · Zbl 1185.68636
[19] G. Sutcliffe, The CADE ATP system competition - CASC, AI Magazine37(2) (2016), 99-101. doi:10.1609/aimag.v37i2. 2620.
[20] G. Sutcliffe, The CADE-26 Automated Theorem Proving System Competition - CASC-26,AI Communications30(6) (2017), 419-432. doi:10.3233/AIC-170744.
[21] G. Sutcliffe,Proceedings of the 9th IJCAR ATP SystemCompetition.Oxford,UnitedKingdom,2018, http://www.tptp.org/CASC/J9/Proceedings.pdf.
[22] G. Sutcliffe and C.B. Suttner, Evaluating general purpose automated theorem proving systems,Artificial Intelligence131(1- 2) (2001), 39-54. doi:10.1016/S0004-3702(01)00113-8. · Zbl 0996.68182
[23] Y.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.