{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,28]],"date-time":"2025-06-28T04:07:22Z","timestamp":1751083642072,"version":"3.41.0"},"reference-count":30,"publisher":"SAGE Publications","issue":"6","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AIC"],"published-print":{"date-parts":[[2017,12,1]]},"DOI":"10.3233\/aic-170744","type":"journal-article","created":{"date-parts":[[2017,11,24]],"date-time":"2017-11-24T15:48:14Z","timestamp":1511538494000},"page":"419-432","source":"Crossref","is-referenced-by-count":9,"title":["The CADE-26 automated theorem proving system competition \u2013 CASC-26"],"prefix":"10.1177","volume":"30","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":"4","key":"10.3233\/AIC-170744_ref1","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/s10817-011-9233-2","article-title":"Analytic tableaux for higher-order logic with choice","volume":"47","author":"Backes","year":"2011","journal-title":"Journal of Automated Reasoning"},{"key":"10.3233\/AIC-170744_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63046-5_27"},{"issue":"1","key":"10.3233\/AIC-170744_ref3","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/s10817-016-9392-2","article-title":"Finding proofs in tarskian geometry","volume":"58","author":"Beeson","year":"2017","journal-title":"Journal of Automated Reasoning"},{"key":"10.3233\/AIC-170744_ref4","doi-asserted-by":"crossref","unstructured":"C.\u00a0Benzm\u00fcller, A.\u00a0Steen and M.\u00a0Wisniewski, Leo-III version 1.1 (system description), in: Proceedings of the IWIL Workshop and LPAR Short Presentations, T.\u00a0Eiter, D.\u00a0Sands, S.\u00a0Schulz, J.\u00a0Urban, G.\u00a0Sutcliffe and A.\u00a0Voronkov, eds, Kalpa Publications in Computing, Vol.\u00a01, 2017.","DOI":"10.29007\/grmx"},{"key":"10.3233\/AIC-170744_ref5","doi-asserted-by":"crossref","unstructured":"J.\u00a0Blanchette, P.\u00a0Fontaine, S.\u00a0Schulz and U.\u00a0Waldmann, Towards strong higher-order automation for fast interactive verification, in: Proceedings of the 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE 2017), G.\u00a0Reger and D.\u00a0Trayfel, eds, EPiC Series in Computing, Vol.\u00a051, EasyChair Publications, 2017, pp.\u00a016\u201323.","DOI":"10.29007\/3ngx"},{"key":"10.3233\/AIC-170744_ref6","doi-asserted-by":"crossref","unstructured":"C.E.\u00a0Brown, Satallax: An automated higher-order prover (system description), in: Proceedings of the 6th International Joint Conference on Automated Reasoning, B.\u00a0Gramlich, D.\u00a0Miller and U.\u00a0Sattler, eds, Lecture Notes in Artificial Intelligence, Vol.\u00a07364, 2012, pp.\u00a0111\u2013117.","DOI":"10.1007\/978-3-642-31365-3_11"},{"issue":"1","key":"10.3233\/AIC-170744_ref7","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s10817-013-9283-8","article-title":"Reducing higher-order theorem proving to a sequence of SAT problems","volume":"51","author":"Brown","year":"2013","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"10.3233\/AIC-170744_ref8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-6(2:3)2010","article-title":"Analytic tableaux for simple type theory and its first-order fragment","volume":"6","author":"Brown","year":"2010","journal-title":"Logical Methods in Computer Science"},{"issue":"1","key":"10.3233\/AIC-170744_ref10","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1023\/A:1027357912519","article-title":"Theorem proving modulo","volume":"31","author":"Dowek","year":"2003","journal-title":"Journal of Automated Reasoning"},{"key":"10.3233\/AIC-170744_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24605-3_37"},{"issue":"1","key":"10.3233\/AIC-170744_ref12","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-170744_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22438-6_23"},{"key":"10.3233\/AIC-170744_ref14","unstructured":"C.\u00a0Kaliszyk, F.\u00a0Chollet and C.\u00a0Szegedy, HolStep: A machine learning dataset for higher-order logic theorem proving, in: Proceedings of the 6th International Conference on Learning Representations (ICRL 2017), I.\u00a0Murray, M.\u00a0Ranzato and O.\u00a0Vinyals, eds, 2018, to appear."},{"key":"10.3233\/AIC-170744_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08434-3_26"},{"key":"10.3233\/AIC-170744_ref16","doi-asserted-by":"crossref","unstructured":"E.\u00a0Kotelnikov, L.\u00a0Kovacsi, G.\u00a0Reger and A.\u00a0Voronkov, The Vampire and the FOOL, in: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, J.\u00a0Avigad and A.\u00a0Chlipala, eds, ACM, New York, 2016, pp.\u00a037\u201348.","DOI":"10.1145\/2854065.2854071"},{"key":"10.3233\/AIC-170744_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"issue":"4","key":"10.3233\/AIC-170744_ref18","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","article-title":"A logic programming language with lambda-abstraction, function variables, and simple unification","volume":"1","author":"Miller","year":"1991","journal-title":"Journal of Logic and Computation"},{"key":"10.3233\/AIC-170744_ref19","doi-asserted-by":"crossref","unstructured":"L.\u00a0Paulson and J.\u00a0Blanchette, 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, G.\u00a0Sutcliffe, E.\u00a0Ternovska and S.\u00a0Schulz, eds, EPiC Series in Computing, Vol.\u00a02, 2010, pp.\u00a01\u201311.","DOI":"10.29007\/36dt"},{"key":"10.3233\/AIC-170744_ref20","doi-asserted-by":"crossref","unstructured":"G.\u00a0Reger, M.\u00a0Suda and A.\u00a0Voronkov, New techniques in clausal form generation, 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.\u00a011\u201323.","DOI":"10.29007\/dzfz"},{"key":"10.3233\/AIC-170744_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36675-8_3"},{"key":"10.3233\/AIC-170744_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-42432-3_10"},{"key":"10.3233\/AIC-170744_ref23","doi-asserted-by":"crossref","unstructured":"A.\u00a0Steen, M.\u00a0Wisniewski and C.\u00a0Benzm\u00fcller, Agent-based HOL reasoning, in: Proceedings of the IWIL Workshop and LPAR Short Presentations, T.\u00a0Eiter, D.\u00a0Sands, G.\u00a0Sutcliffe and A.\u00a0Voronkov, eds, Kalpa Publications in Computing, Vol.\u00a01, 2016.","DOI":"10.1007\/978-3-319-42432-3_10"},{"key":"10.3233\/AIC-170744_ref24","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-170744_ref25","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-170744_ref26","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-170744_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_1"},{"key":"10.3233\/AIC-170744_ref28","unstructured":"G.\u00a0Sutcliffe, Proceedings of the 8th IJCAR ATP System Competition (CASC-J8), Coimbra, Portugal, 2016, http:\/\/www.tptp.org\/CASC\/J8\/Proceedings.pdf."},{"issue":"5","key":"10.3233\/AIC-170744_ref29","doi-asserted-by":"publisher","first-page":"607","DOI":"10.3233\/AIC-160709","article-title":"The 8th IJCAR automated theorem proving system competition \u2013 CASC-J8","volume":"29","author":"Sutcliffe","year":"2016","journal-title":"AI Communications"},{"issue":"2","key":"10.3233\/AIC-170744_ref30","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":"1\u20132","key":"10.3233\/AIC-170744_ref31","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-170744","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,27]],"date-time":"2025-06-27T13:50:16Z","timestamp":1751032216000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/AIC-170744"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,1]]},"references-count":30,"journal-issue":{"issue":"6"},"URL":"https:\/\/doi.org\/10.3233\/aic-170744","relation":{},"ISSN":["1875-8452","0921-7126"],"issn-type":[{"type":"electronic","value":"1875-8452"},{"type":"print","value":"0921-7126"}],"subject":[],"published":{"date-parts":[[2017,12,1]]}}}