{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T04:13:06Z","timestamp":1749701586869,"version":"3.41.0"},"reference-count":24,"publisher":"SAGE Publications","issue":"5","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AIC"],"published-print":{"date-parts":[[2016,11,15]]},"DOI":"10.3233\/aic-160709","type":"journal-article","created":{"date-parts":[[2016,10,18]],"date-time":"2016-10-18T14:16:00Z","timestamp":1476800160000},"page":"607-619","source":"Crossref","is-referenced-by-count":14,"title":["The 8th IJCAR automated theorem proving system competition\u00a0\u2013 CASC-J8"],"prefix":"10.1177","volume":"29","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":[{"key":"10.3233\/AIC-160709_ref1","doi-asserted-by":"crossref","unstructured":"T.\u00a0Gauthier and C.\u00a0Kaliszyk, Premise selection and external provers for HOL4, in: Proceedings of the 4th ACM SIGPLAN Conference on Certified Programs and Proofs, X.\u00a0Leroy and A.\u00a0Tiu, eds, ACM Press, 2015, pp.\u00a049\u201357.","DOI":"10.1145\/2676724.2693173"},{"issue":"1","key":"10.3233\/AIC-160709_ref2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s00454-009-9148-4","article-title":"A revision of the proof of the Kepler conjecture","volume":"44","author":"Hales","year":"2010","journal-title":"Discrete and Computational Geometry"},{"key":"10.3233\/AIC-160709_ref3","doi-asserted-by":"crossref","unstructured":"K.\u00a0Hoder and A.\u00a0Voronkov, Sine qua non for large theory reasoning, in: Proceedings of the 23rd International Conference on Automated Deduction, V.\u00a0Sofronie-Stokkermans and N.\u00a0Bj\u0153rner, eds, Lecture Notes in Artificial Intelligence, Vol.\u00a06803, Springer-Verlag, 2011, pp.\u00a0299\u2013314.","DOI":"10.1007\/978-3-642-22438-6_23"},{"key":"10.3233\/AIC-160709_ref4","doi-asserted-by":"crossref","unstructured":"J.\u00a0Harrison, HOL light: An overview, in: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, T.\u00a0Nipkow and C.\u00a0Urban, eds, Lecture Notes in Computer Science, Vol.\u00a05674, Springer-Verlag, 2009, pp.\u00a060\u201366.","DOI":"10.1007\/978-3-642-03359-9_4"},{"key":"10.3233\/AIC-160709_ref5","unstructured":"C.\u00a0Kaliszyk, G.\u00a0Sutcliffe and F.\u00a0Rabe, TH1: The TPTP typed higher-order form with rank-1 polymorphism, in: Proceedings of the 5th Workshop on the Practical Aspects of Automated Reasoning, P.\u00a0Fontaine, S.\u00a0Schulz and J.\u00a0Urban, eds, CEUR Workshop Proceedings, Vol.\u00a01653, 2016, pp.\u00a041\u201355."},{"key":"10.3233\/AIC-160709_ref6","doi-asserted-by":"crossref","unstructured":"Z.\u00a0Khasidashvili and K.\u00a0Korovin, Predicate elimination for preprocessing in first-order theorem proving, in: Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing, N.\u00a0Creignou and D.\u00a0Le Berre, eds, Lecture Notes in Computer Science, Vol.\u00a09710, Springer-Verlag, 2016, pp.\u00a0361\u2013372.","DOI":"10.1007\/978-3-319-40970-2_22"},{"key":"10.3233\/AIC-160709_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36675-8_8"},{"key":"10.3233\/AIC-160709_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"10.3233\/AIC-160709_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"10.3233\/AIC-160709_ref11","doi-asserted-by":"crossref","unstructured":"G.\u00a0Reger, N.\u00a0Bj\u00f8rner, M.\u00a0Suda and A.\u00a0Voronkov, AVATAR modulo theories, in: Proceedings of the 2nd Global Conference on Artificial Intelligence, C.\u00a0Benzm\u00fcller, G.\u00a0Sutcliffe and R.\u00a0Rojas, eds, EPiC Series in Computing, Vol.\u00a041, EasyChair Publications, 2016, pp.\u00a039\u201352.","DOI":"10.29007\/k6tp"},{"key":"10.3233\/AIC-160709_ref12","doi-asserted-by":"crossref","unstructured":"G.\u00a0Reger, M.\u00a0Suda and A.\u00a0Voronkov, Finding finite models in multi-sorted first order logic, in: Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing, N.\u00a0Creignou and D.\u00a0Le Berre, eds, Lecture Notes in Computer Science, Springer-Verlag, 2016.","DOI":"10.1007\/978-3-319-40970-2_20"},{"key":"10.3233\/AIC-160709_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"10.3233\/AIC-160709_ref14","doi-asserted-by":"crossref","unstructured":"A.\u00a0Steen, M.\u00a0Wisniewski and C.\u00a0Benzm\u00fcller, Agent-based HOL reasoning, in: Proceedings of the 5th International Congress on Mathematical Software, G.-M.\u00a0Greuel, T.\u00a0Koch, P.\u00a0Paule and A.\u00a0Sommese, eds, Lecture Notes in Computer Science, Vol.\u00a09725, Springer-Verlag, 2016, pp.\u00a075\u201381.","DOI":"10.1007\/978-3-319-42432-3_10"},{"key":"10.3233\/AIC-160709_ref15","doi-asserted-by":"crossref","unstructured":"A.\u00a0Stump, G.\u00a0Sutcliffe and C.\u00a0Tinelli, StarExec: A cross-community infrastructure for logic solving, in: Proceedings of the 7th International Joint Conference on Automated Reasoning, S.\u00a0Demri, D.\u00a0Kapur and C.\u00a0Weidenbach, eds, Lecture Notes in Artificial Intelligence, Vol.\u00a08562, 2014, pp.\u00a0367\u2013373.","DOI":"10.1007\/978-3-319-08587-6_28"},{"issue":"3","key":"10.3233\/AIC-160709_ref16","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"},{"issue":"4","key":"10.3233\/AIC-160709_ref17","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"},{"key":"10.3233\/AIC-160709_ref18","unstructured":"G.\u00a0Sutcliffe, in: Proceedings of the 8th IJCAR ATP System Competition, Coimbra, Portugal, 2016, http:\/\/www.tptp.org\/CASC\/J8\/Proceedings.pdf."},{"issue":"2","key":"10.3233\/AIC-160709_ref19","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1609\/aimag.v37i2.2620","article-title":"The CADE ATP system competition\u00a0\u2013 CASC","volume":"37","author":"Sutcliffe","year":"2016","journal-title":"AI Magazine"},{"key":"10.3233\/AIC-160709_ref20","doi-asserted-by":"crossref","unstructured":"G.\u00a0Sutcliffe and S.\u00a0Schulz, The thousands of models for theorem provers (TMTP) model library\u00a0\u2013 First steps, in: Proceedings of the 11th International Workshop on the Implementation of Logics, B.\u00a0Konev, S.\u00a0Schulz and L.\u00a0Simon, eds, EPiC Series in Computing, Vol.\u00a040, EasyChair Publications, 2016, pp.\u00a0106\u2013121.","DOI":"10.29007\/7dg5"},{"issue":"1\u20132","key":"10.3233\/AIC-160709_ref21","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"},{"issue":"3","key":"10.3233\/AIC-160709_ref22","doi-asserted-by":"publisher","first-page":"423","DOI":"10.3233\/AIC-150691","article-title":"The CADE-25 automated theorem proving system competition\u00a0\u2013 CASC-25","volume":"29","author":"Sutcliffe","year":"2016","journal-title":"AI Communications"},{"issue":"3","key":"10.3233\/AIC-160709_ref23","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/BF00252178","article-title":"Using hints to increase the effectiveness of an automated reasoning program: Case studies","volume":"16","author":"Veroff","year":"1996","journal-title":"Journal of Automated Reasoning"},{"key":"10.3233\/AIC-160709_ref24","doi-asserted-by":"crossref","unstructured":"M.\u00a0Wisniewski, A.\u00a0Steen and C.\u00a0Benzm\u00fcller, LeoPARD\u00a0\u2013 A generic platform for the implementation of higher-order reasoners, in: Proceedings of the International Conference on Intelligent Computer Mathematics, M.\u00a0Kerber, J.\u00a0Carette, C.\u00a0Kaliszyk, F.\u00a0Rabe and V.\u00a0Sorge, eds, Lecture Notes in Computer Science, Vol.\u00a09150, Springer-Verlag, 2015, pp.\u00a0325\u2013330.","DOI":"10.1007\/978-3-319-20615-8_22"},{"key":"10.3233\/AIC-160709_ref25","doi-asserted-by":"crossref","unstructured":"M.\u00a0Wisniewski, A.\u00a0Steen, K.\u00a0Kern and C.\u00a0Benzm\u00fcller, Effective normalization techniques for HOL, in: Proceedings of the 8th International Joint Conference on Automated Reasoning, N.\u00a0Olivetti and A.\u00a0Tiwari, eds, Lecture Notes in Artificial Intelligence, Vol.\u00a09706, 2016, pp.\u00a0362\u2013370.","DOI":"10.1007\/978-3-319-40229-1_25"}],"container-title":["AI Communications"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/AIC-160709","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T16:33:16Z","timestamp":1749659596000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/AIC-160709"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11,15]]},"references-count":24,"journal-issue":{"issue":"5"},"URL":"https:\/\/doi.org\/10.3233\/aic-160709","relation":{},"ISSN":["1875-8452","0921-7126"],"issn-type":[{"type":"electronic","value":"1875-8452"},{"type":"print","value":"0921-7126"}],"subject":[],"published":{"date-parts":[[2016,11,15]]}}}