{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:10:52Z","timestamp":1750306252482,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":17,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,1,16]],"date-time":"2017-01-16T00:00:00Z","timestamp":1484524800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100010663","name":"H2020 European Research Council","doi-asserted-by":"publisher","award":["649043"],"award-info":[{"award-number":["649043"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,1,16]]},"DOI":"10.1145\/3018610.3018619","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T21:20:29Z","timestamp":1482441629000},"page":"43-52","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["BliStrTune: hierarchical invention of theorem proving strategies"],"prefix":"10.1145","author":[{"given":"Jan","family":"Jakub\u016fv","sequence":"first","affiliation":[{"name":"Czech Technical University, Czech Republic"}]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[{"name":"Czech Technical University, Czech Republic"}]}],"member":"320","published-online":{"date-parts":[[2017,1,16]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9286-5"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9362-8"},{"issue":"2","key":"e_1_3_2_1_3_1","first-page":"153","volume":"3","author":"Grabowski A.","year":"2010","unstructured":"A. Grabowski , A. Korni\u0142owicz , and A. Naumowicz . Mizar in a nutshell. J. Formalized Reasoning , 3 ( 2 ): 153 \u2013 245 , 2010 . A. Grabowski, A. Korni\u0142owicz, and A. Naumowicz. Mizar in a nutshell. J. Formalized Reasoning, 3(2):153\u2013245, 2010.","journal-title":"Mizar in a nutshell. J. Formalized Reasoning"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1734953.1734959"},{"key":"e_1_3_2_1_5_1","first-page":"156","volume-title":"CICM 2016, Bialystok, Poland, July 25-29, 2016","author":"Jakub\u02dauv J.","year":"2016","unstructured":"J. Jakub\u02dauv and J. Urban . Extending E prover with similarity based clause selection strategies. In Intelligent Computer Mathematics - 9th International Conference , CICM 2016, Bialystok, Poland, July 25-29, 2016 , Proceedings , pages 151\u2013 156 , 2016 . J. Jakub\u02dauv and J. Urban. Extending E prover with similarity based clause selection strategies. In Intelligent Computer Mathematics - 9th International Conference, CICM 2016, Bialystok, Poland, July 25-29, 2016, Proceedings, pages 151\u2013156, 2016."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-014-9303-3"},{"key":"e_1_3_2_1_7_1","first-page":"707","volume":"10","author":"Levenshtein V.","year":"1966","unstructured":"V. Levenshtein . Binary Codes Capable of Correcting Deletions , Insertions and Reversals. Soviet Physics Doklady , 10 : 707 , 1966 . V. Levenshtein. Binary Codes Capable of Correcting Deletions, Insertions and Reversals. Soviet Physics Doklady, 10:707, 1966.","journal-title":"Insertions and Reversals. Soviet Physics Doklady"},{"key":"e_1_3_2_1_8_1","first-page":"664","volume-title":"International Conference on Automated Deduction","author":"McCune W.","unstructured":"W. McCune . Otter 2.0. In International Conference on Automated Deduction , pages 663\u2013 664 . Springer, 1990. W. McCune. Otter 2.0. In International Conference on Automated Deduction, pages 663\u2013664. Springer, 1990."},{"key":"e_1_3_2_1_9_1","volume-title":"0 users","author":"McCune W. W.","year":"1989","unstructured":"W. W. McCune . Otter 1. 0 users \u2019 guide. Technical report, Argonne National Lab., IL (USA) , 1989 . W. W. McCune. Otter 1. 0 users\u2019 guide. Technical report, Argonne National Lab., IL (USA), 1989."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"W. W. McCune. Otter 3.0 reference manual and guide volume 9700. Argonne National Laboratory Argonne IL 1994. W. W. McCune. Otter 3.0 reference manual and guide volume 9700. Argonne National Laboratory Argonne IL 1994.","DOI":"10.2172\/10129052"},{"key":"e_1_3_2_1_11_1","volume-title":"Global Conference on Artificial Intelligence, GCAI 2015","volume":"36","author":"Sch\u00e4fer S.","year":"2015","unstructured":"S. Sch\u00e4fer and S. Schulz . Breeding theorem proving heuristics with genetic algorithms. In G. Gottlob, G. Sutcliffe, and A. Voronkov, editors , Global Conference on Artificial Intelligence, GCAI 2015 , Tbilisi, Georgia , October 16-19, 2015 , volume 36 of EPiC Series in Computing, pages 263\u2013274. EasyChair, 2015. S. Sch\u00e4fer and S. Schulz. Breeding theorem proving heuristics with genetic algorithms. In G. Gottlob, G. Sutcliffe, and A. Voronkov, editors, Global Conference on Artificial Intelligence, GCAI 2015, Tbilisi, Georgia, October 16-19, 2015, volume 36 of EPiC Series in Computing, pages 263\u2013274. EasyChair, 2015."},{"key":"e_1_3_2_1_12_1","first-page":"735","volume":"8312","author":"Schulz S.","year":"2013","unstructured":"S. Schulz . System description: E 1.8. In K. L. McMillan , A. Middeldorp , and A. Voronkov , editors, LPAR , volume 8312 of LNCS, pages 735 \u2013 743 . Springer, 2013 . ISBN 978-3-642-45220-8. S. Schulz. System description: E 1.8. In K. L. McMillan, A. Middeldorp, and A. Voronkov, editors, LPAR, volume 8312 of LNCS, pages 735\u2013743. Springer, 2013. ISBN 978-3-642-45220-8.","journal-title":"editors, LPAR"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-004-6245-1"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-006-9032-3"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"J. Urban . BliStr: The Blind Strategymaker . In G. Gottlob G. Sutcliffe and A. Voronkov editors GCAI 2015 . Global Conference on Artificial Intelligence volume 36 of EPiC Series in Computing pages 312\u2013 319 . EasyChair 2015. J. Urban. BliStr: The Blind Strategymaker. In G. Gottlob G. Sutcliffe and A. Voronkov editors GCAI 2015. Global Conference on Artificial Intelligence volume 36 of EPiC Series in Computing pages 312\u2013319. EasyChair 2015.","DOI":"10.29007\/8n7m"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_37"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1137\/0218082"}],"event":{"name":"CPP '17: Certified Proofs and Programs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"Paris France","acronym":"CPP '17"},"container-title":["Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3018610.3018619","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3018610.3018619","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:23:59Z","timestamp":1750220639000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3018610.3018619"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1,16]]},"references-count":17,"alternative-id":["10.1145\/3018610.3018619","10.1145\/3018610"],"URL":"https:\/\/doi.org\/10.1145\/3018610.3018619","relation":{},"subject":[],"published":{"date-parts":[[2017,1,16]]},"assertion":[{"value":"2017-01-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}