{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,19]],"date-time":"2025-09-19T09:35:25Z","timestamp":1758274525302,"version":"3.38.0"},"reference-count":33,"publisher":"SAGE Publications","issue":"5-6","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AIC"],"published-print":{"date-parts":[[2020,3,4]]},"DOI":"10.3233\/aic-190627","type":"journal-article","created":{"date-parts":[[2020,3,6]],"date-time":"2020-03-06T15:12:19Z","timestamp":1583507539000},"page":"373-389","source":"Crossref","is-referenced-by-count":8,"title":["The CADE-27 Automated theorem proving System Competition \u2013 CASC-27"],"prefix":"10.1177","volume":"32","author":[{"given":"Geoff","family":"Sutcliffe","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Miami, USA. E-mail:\u00a0geoff@cs.miami.edu"}]}],"member":"179","reference":[{"issue":"2","key":"10.3233\/AIC-190627_ref1","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10817-013-9286-5","article-title":"Premise selection for mathematics by corpus analysis and kernel methods","volume":"52","author":"Alama","year":"2014","journal-title":"Journal of Automated Reasoning"},{"key":"10.3233\/AIC-190627_ref2","unstructured":"H. Barbosa, A. Reynolds, D. El Ouraoui, C. Tinelli and C. Barrett, Extending SMT solvers to higher-order logic, in: Proceedings of the 27th International Conference on Automated Deduction, P. Fontaine, ed., Lecture Notes in Computer Science, Vol. 11716, Springer-Verlag, 2019, pp. 35\u201354."},{"key":"10.3233\/AIC-190627_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"10.3233\/AIC-190627_ref4","doi-asserted-by":"crossref","unstructured":"E. Bartocci, D. Beyer, P.E. Black, G. Fedyukovich, H. Garavel, A. Hartmanns, M. Huisman, F. Kordon, J. Nagele, M. Sighireanu, B. Steffen, M. Suda, G. Sutcliffe, T. Weber and A. 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, T. Vojnar and L. Zhang, eds, Lecture Notes in Computer Science, Vol. 11429, Springer-Verlag, 2019, page to appear.","DOI":"10.1007\/978-3-030-17502-3_1"},{"key":"10.3233\/AIC-190627_ref5","unstructured":"A. Bhayat and G. 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, B. Konev, P. R\u00fcmmer and J. Urban, eds, 2018, pp. 2\u201316."},{"key":"10.3233\/AIC-190627_ref6","unstructured":"A. Bhayat and G. Reger, Restricted combinatory unification, in: Proceedings of the 27th International Conference on Automated Deduction, P. Fontaine, ed., Lecture Notes in Computer Science, Vol. 11716, Springer-Verlag, 2019, pp. 74\u201393."},{"key":"10.3233\/AIC-190627_ref7","unstructured":"C. Brown, T. Gauthier, C. Kaliszyk, G. Sutcliffe and J. Urban, GRUNGE: A grand unified ATP challenge, in: Proceedings of the 27th International Conference on Automated Deduction, P. Fontaine, ed., Lecture Notes in Computer Science, Vol. 11716, Springer-Verlag, 2019, pp. 123\u2013141."},{"key":"10.3233\/AIC-190627_ref8","unstructured":"K. Claessen and N. Smallbone, Efficient encodings of first-order 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\u2013404."},{"key":"10.3233\/AIC-190627_ref9","unstructured":"K. Claessen and N. S\u00f6rensson, New techniques that improve MACE-style finite model finding, in: Proceedings of the CADE-19 Workshop: Model Computation \u2013 Principles, Algorithms, Applications, P. Baumgartner and C. Fermueller, eds, 2003."},{"key":"10.3233\/AIC-190627_ref11","doi-asserted-by":"crossref","unstructured":"T. Gauthier and C. Kaliszyk, Premise selection and external provers for HOL4, in: Proceedings of the 4th ACM SIGPLAN Conference on Certified Programs and Proofs, X. Leroy and A. Tiu, eds, ACM Press, 2015, pp. 49\u201357.","DOI":"10.1145\/2676724.2693173"},{"key":"10.3233\/AIC-190627_ref12","unstructured":"K. Hoder and A. Voronkov, Sine qua non for large theory reasoning, in: Proceedings of the 23rd International Conference on Automated Deduction, V. Sofronie-Stokkermans and N. Bj\u0153rner, eds, Lecture Notes in Artificial Intelligence, Vol. 6803, Springer-Verlag, 2011, pp. 299\u2013314."},{"key":"10.3233\/AIC-190627_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96812-4_11"},{"key":"10.3233\/AIC-190627_ref14","unstructured":"J. Jakubuv and J. 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."},{"issue":"2","key":"10.3233\/AIC-190627_ref15","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/0304-3975(76)90021-9","article-title":"Mechanizing omega-order type theory through unification","volume":"3","author":"Jensen","year":"1976","journal-title":"Theoretical Computer Science"},{"key":"10.3233\/AIC-190627_ref16","doi-asserted-by":"crossref","unstructured":"E. Kotelnikov, L. Kovacs, G. Reger and A. Voronkov, The vampire and the FOOL, in: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, J. Avigad and A. Chlipala, eds, ACM, 2016, pp. 37\u201348.","DOI":"10.1145\/2854065.2854071"},{"key":"10.3233\/AIC-190627_ref17","unstructured":"D. K\u00fclwein, T. van Laarhoven, E. Tsivtsivadze, J. Urban and T. Heskes, Overview and evaluation of premise selection techniques for large theory mathematics, in: Proceedings of the 6th International Joint Conference on Automated Reasoning, B. Gramlich, D. Miller and U. Sattler, eds, Lecture Notes in Artificial Intelligence, Vol. 7364, 2012, pp. 378\u2013392."},{"issue":"6","key":"10.3233\/AIC-190627_ref18","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","article-title":"Solving SAT and SAT modulo theories: From an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T)","volume":"53","author":"Nieuwenhuis","year":"2006","journal-title":"Journal of the ACM"},{"key":"10.3233\/AIC-190627_ref19","unstructured":"M. Rawson and G. 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, B. Konev, P. R\u00fcmmer and J. Urban, eds, 2018, pp. 58\u201371."},{"key":"10.3233\/AIC-190627_ref20","unstructured":"M. Rawson and G. Reger, Old or heavy? Decaying gracefully with age\/weight shapes, in: Proceedings of the 27th International Conference on Automated Deduction, P. Fontaine, ed., Lecture Notes in Computer Science, Vol. 11716, Springer-Verlag, 2019, pp. 462\u2013476."},{"key":"10.3233\/AIC-190627_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29007-8_1"},{"key":"10.3233\/AIC-190627_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66167-4_2"},{"key":"10.3233\/AIC-190627_ref23","unstructured":"S. Schulz, S. Cruanes and P. Vukmirovic, Faster, higher, stronger: E 2.3, in: Proceedings of the 27th International Conference on Automated Deduction, P. Fontaine, ed., Lecture Notes in Computer Science, Vol. 11716, Springer-Verlag, 2019, pp. 495\u2013507."},{"key":"10.3233\/AIC-190627_ref24","unstructured":"S. Schulz and M. M\u00f6hrmann, Performance of clause selection heuristics for saturation-based theorem proving, 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. 330\u2013345."},{"key":"10.3233\/AIC-190627_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"10.3233\/AIC-190627_ref26","unstructured":"P. Smith, An Introduction to Goedel\u2019s Theorems, Cambridge University Press, 2007."},{"key":"10.3233\/AIC-190627_ref27","unstructured":"A. Stump, G. Sutcliffe and C. Tinelli, StarExec: A cross-community 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\u2013373."},{"issue":"3","key":"10.3233\/AIC-190627_ref28","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1023\/A:1006393501098","article-title":"The CADE-16 ATP system competition","volume":"24","author":"Sutcliffe","year":"2000","journal-title":"Journal of Automated Reasoning"},{"key":"10.3233\/AIC-190627_ref29","unstructured":"G. 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, G. Sutcliffe, P. Rudnicki, R. Schmidt, B. Konev and S. Schulz, eds, 2008, pp. 38\u201349."},{"issue":"4","key":"10.3233\/AIC-190627_ref30","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","article-title":"The TPTP problem library and associated infrastructure. The FOF and CNF parts, v3.5.0","volume":"43","author":"Sutcliffe","year":"2009","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"10.3233\/AIC-190627_ref31","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1609\/aimag.v37i2.2620","article-title":"The CADE ATP system competition \u2013 CASC","volume":"37","author":"Sutcliffe","year":"2016","journal-title":"AI Magazine"},{"issue":"6","key":"10.3233\/AIC-190627_ref32","doi-asserted-by":"publisher","first-page":"495","DOI":"10.3233\/AIC-180773","article-title":"The 9th IJCAR automated theorem proving system competition \u2013 CASC-J9","volume":"31","author":"Sutcliffe","year":"2018","journal-title":"AI Communications"},{"key":"10.3233\/AIC-190627_ref34","unstructured":"G. Sutcliffe, S. Schulz, K. Claessen and A. Van Gelder, Using the TPTP language for writing derivations and finite interpretations, in: Proceedings of the 3rd International Joint Conference on Automated Reasoning, U. Furbach and N. Shankar, eds, Lecture Notes in Artificial Intelligence, Vol. 4130, 2006, pp. 67\u201381."},{"issue":"1\u20132","key":"10.3233\/AIC-190627_ref35","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S0004-3702(01)00113-8","article-title":"Evaluating general purpose automated theorem proving systems","volume":"131","author":"Sutcliffe","year":"2001","journal-title":"Artificial Intelligence"}],"container-title":["AI Communications"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/AIC-190627","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,10]],"date-time":"2025-03-10T14:31:02Z","timestamp":1741617062000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/AIC-190627"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,3,4]]},"references-count":33,"journal-issue":{"issue":"5-6"},"URL":"https:\/\/doi.org\/10.3233\/aic-190627","relation":{},"ISSN":["1875-8452","0921-7126"],"issn-type":[{"type":"electronic","value":"1875-8452"},{"type":"print","value":"0921-7126"}],"subject":[],"published":{"date-parts":[[2020,3,4]]}}}