{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T06:56:44Z","timestamp":1760597804769,"version":"3.41.0"},"reference-count":30,"publisher":"SAGE Publications","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AIC"],"published-print":{"date-parts":[[2018,5,17]]},"DOI":"10.3233\/aic-180761","type":"journal-article","created":{"date-parts":[[2018,4,10]],"date-time":"2018-04-10T15:17:02Z","timestamp":1523373422000},"page":"237-250","source":"Crossref","is-referenced-by-count":12,"title":["Hierarchical invention of theorem proving strategies"],"prefix":"10.1177","volume":"31","author":[{"given":"Jan","family":"Jakub\u016fv","sequence":"first","affiliation":[{"name":"CIIRC, Czech Technical University in Prague, Czech Republic. E-mails:\u00a0jakubuv@gmail.com,\u00a0josef.urban@gmail.com"}]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[{"name":"CIIRC, Czech Technical University in Prague, Czech Republic. E-mails:\u00a0jakubuv@gmail.com,\u00a0josef.urban@gmail.com"}]}],"member":"179","reference":[{"issue":"2","key":"10.3233\/AIC-180761_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":"J. Autom. Reasoning"},{"issue":"1","key":"10.3233\/AIC-180761_ref2","first-page":"101","article-title":"Hammering towards QED","volume":"9","author":"Blanchette","year":"2016","journal-title":"Journal of Formalized Reasoning"},{"issue":"3","key":"10.3233\/AIC-180761_ref3","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10817-016-9362-8","article-title":"A learning-based fact selector for Isabelle\/HOL","volume":"57","author":"Blanchette","year":"2016","journal-title":"J. Autom. Reasoning"},{"key":"10.3233\/AIC-180761_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693173"},{"issue":"2","key":"10.3233\/AIC-180761_ref5","first-page":"153","article-title":"Mizar in a nutshell","volume":"3","author":"Grabowski","year":"2010","journal-title":"J. Formalized Reasoning"},{"key":"10.3233\/AIC-180761_ref6","doi-asserted-by":"crossref","unstructured":"K.\u00a0Hoder and A.\u00a0Voronkov, Sine qua non for large theory reasoning, in: CADE, N.\u00a0Bj\u00f8rner and V.\u00a0Sofronie-Stokkermans, eds, LNCS, Vol.\u00a06803, Springer, 2011, pp.\u00a0299\u2013314.","DOI":"10.1007\/978-3-642-22438-6_23"},{"key":"10.3233\/AIC-180761_ref7","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1613\/jair.2861","article-title":"ParamILS: An automatic algorithm configuration framework","volume":"36","author":"Hutter","year":"2009","journal-title":"J. Artificial Intelligence Research"},{"key":"10.3233\/AIC-180761_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-42547-4_11"},{"key":"10.3233\/AIC-180761_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018619"},{"issue":"2","key":"10.3233\/AIC-180761_ref10","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-014-9303-3","article-title":"Learning-assisted automated reasoning with Flyspeck","volume":"53","author":"Kaliszyk","year":"2014","journal-title":"J. Autom. Reasoning"},{"issue":"3","key":"10.3233\/AIC-180761_ref11","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s10817-015-9330-8","article-title":"MizAR 40 for Mizar 40","volume":"55","author":"Kaliszyk","year":"2015","journal-title":"J. Autom. Reasoning"},{"key":"10.3233\/AIC-180761_ref12","unstructured":"C.\u00a0Kaliszyk, J.\u00a0Urban and J.\u00a0Vyskocil, Efficient semantic features for automated reasoning over large theories, in: IJCAI\u201915, Q.\u00a0Yang and M.\u00a0Wooldridge, eds, AAAI Press, 2015, pp.\u00a03084\u20133090."},{"key":"10.3233\/AIC-180761_ref13","doi-asserted-by":"crossref","unstructured":"C.\u00a0Kaliszyk, J.\u00a0Urban and J.\u00a0Vyskocil, Machine learner for automated reasoning 0.4 and 0.5, in: PAAR-2014. 4th Workshop on Practical Aspects of Automated Reasoning, S.\u00a0Schulz, L.D.\u00a0Moura and B.\u00a0Konev, eds, EPiC Series in Computing, Vol.\u00a031, EasyChair, 2015, pp.\u00a060\u201366.","DOI":"10.29007\/shxj"},{"key":"10.3233\/AIC-180761_ref14","doi-asserted-by":"crossref","unstructured":"L.\u00a0Kov\u00e1cs and A.\u00a0Voronkov, First-order theorem proving and Vampire, in: CAV, N.\u00a0Sharygina and H.\u00a0Veith, eds, LNCS, Vol.\u00a08044, Springer, 2013, pp.\u00a01\u201335.","DOI":"10.1007\/978-3-642-39799-8_1"},{"issue":"2","key":"10.3233\/AIC-180761_ref15","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/s10817-015-9329-1","article-title":"MaLeS: A framework for automatic tuning of automated theorem provers","volume":"55","author":"K\u00fchlwein","year":"2015","journal-title":"J. Autom. Reasoning"},{"key":"10.3233\/AIC-180761_ref16","doi-asserted-by":"crossref","unstructured":"J.\u00a0Leskovec, A.\u00a0Rajaraman and J.D.\u00a0Ullman, Mining of Massive Datasets, 2nd edn, Cambridge University Press, 2014.","DOI":"10.1017\/CBO9781139924801"},{"key":"10.3233\/AIC-180761_ref17","first-page":"707","article-title":"Binary codes capable of correcting deletions, insertions and reversals","volume":"10","author":"Levenshtein","year":"1966","journal-title":"Soviet Physics Doklady"},{"key":"10.3233\/AIC-180761_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52885-7_131"},{"key":"10.3233\/AIC-180761_ref20","doi-asserted-by":"crossref","unstructured":"W.W.\u00a0McCune, Otter 3.0 Reference Manual and Guide, Vol.\u00a09700, Argonne National Laboratory, Argonne, IL, 1994.","DOI":"10.2172\/10129052"},{"key":"10.3233\/AIC-180761_ref21","unstructured":"S.\u00a0Sch\u00e4fer and S.\u00a0Schulz, Breeding theorem proving heuristics with genetic algorithms, in: Global Conference on Artificial Intelligence, GCAI, 2015, Tbilisi, Georgia, October 16\u201319, 2015, G.\u00a0Gottlob, G.\u00a0Sutcliffe and A.\u00a0Voronkov, eds, EPiC Series in Computing, Vol.\u00a036, EasyChair, 2015, pp.\u00a0263\u2013274."},{"issue":"2","key":"10.3233\/AIC-180761_ref22","first-page":"111","article-title":"E\u00a0\u2013 A brainiac theorem prover","volume":"15","author":"Schulz","year":"2002","journal-title":"AI Communications"},{"key":"10.3233\/AIC-180761_ref23","unstructured":"S.\u00a0Schulz, System description: E 1.8, in: LPAR, K.L.\u00a0McMillan, A.\u00a0Middeldorp and A.\u00a0Voronkov, eds, LNCS, Vol.\u00a08312, Springer, 2013, pp.\u00a0735\u2013743."},{"issue":"2","key":"10.3233\/AIC-180761_ref24","doi-asserted-by":"crossref","first-page":"211","DOI":"10.3233\/AIC-130550","article-title":"The 6th IJCAR automated theorem proving system competition\u00a0\u2013 CASC-J6","volume":"26","author":"Sutcliffe","year":"2013","journal-title":"AI Commun."},{"issue":"1","key":"10.3233\/AIC-180761_ref25","first-page":"42","article-title":"Gnu parallel\u00a0\u2013 the command-line power tool","volume":"36","author":"Tange","year":"2011","journal-title":"; login: The USENIX Magazine"},{"issue":"3\u20134","key":"10.3233\/AIC-180761_ref26","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/s10817-004-6245-1","article-title":"MPTP\u00a0\u2013 Motivation, implementation, first experiments","volume":"33","author":"Urban","year":"2004","journal-title":"J. Autom. Reasoning"},{"issue":"1\u20132","key":"10.3233\/AIC-180761_ref27","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s10817-006-9032-3","article-title":"MPTP 0.2: Design, implementation, and initial experiments","volume":"37","author":"Urban","year":"2006","journal-title":"J. Autom. Reasoning"},{"key":"10.3233\/AIC-180761_ref28","doi-asserted-by":"crossref","unstructured":"J.\u00a0Urban, BliStr: The blind strategymaker, in: GCAI 2015. Global Conference on Artificial Intelligence, G.\u00a0Gottlob, G.\u00a0Sutcliffe and A.\u00a0Voronkov, eds, EPiC Series in Computing, Vol.\u00a036, EasyChair, 2015, pp.\u00a0312\u2013319.","DOI":"10.29007\/8n7m"},{"key":"10.3233\/AIC-180761_ref29","doi-asserted-by":"crossref","unstructured":"J.\u00a0Urban, G.\u00a0Sutcliffe, P.\u00a0Pudl\u00e1k and J.\u00a0Vysko\u010dil, MaLARea SG1\u00a0\u2013 Machine learner for automated reasoning with semantic guidance, in: IJCAR, A.\u00a0Armando, P.\u00a0Baumgartner and G.\u00a0Dowek, eds, LNCS, Vol.\u00a05195, Springer, 2008, pp.\u00a0441\u2013456.","DOI":"10.1007\/978-3-540-71070-7_37"},{"key":"10.3233\/AIC-180761_ref30","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1613\/jair.4806","article-title":"Bayesian optimization in a billion dimensions via random embeddings","volume":"55","author":"Wang","year":"2016","journal-title":"Journal of Artificial Intelligence Research"},{"issue":"6","key":"10.3233\/AIC-180761_ref31","doi-asserted-by":"publisher","first-page":"1245","DOI":"10.1137\/0218082","article-title":"Simple fast algorithms for the editing distance between trees and related problems","volume":"18","author":"Zhang","year":"1989","journal-title":"SIAM J. Comput."}],"container-title":["AI Communications"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/AIC-180761","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,3]],"date-time":"2025-07-03T15:20:16Z","timestamp":1751556016000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/AIC-180761"}},"subtitle":[],"editor":[{"given":"Pascal","family":"Fontaine","sequence":"additional","affiliation":[]},{"given":"Cezary","family":"Kaliszyk","sequence":"additional","affiliation":[]},{"given":"Stephan","family":"Schulz","sequence":"additional","affiliation":[]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[]}],"short-title":[],"issued":{"date-parts":[[2018,5,17]]},"references-count":30,"journal-issue":{"issue":"3"},"URL":"https:\/\/doi.org\/10.3233\/aic-180761","relation":{},"ISSN":["1875-8452","0921-7126"],"issn-type":[{"type":"electronic","value":"1875-8452"},{"type":"print","value":"0921-7126"}],"subject":[],"published":{"date-parts":[[2018,5,17]]}}}