{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:35:18Z","timestamp":1762324518070,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":11,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,7,13]],"date-time":"2019-07-13T00:00:00Z","timestamp":1562976000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,7,13]]},"DOI":"10.1145\/3319619.3321921","type":"proceedings-article","created":{"date-parts":[[2019,7,10]],"date-time":"2019-07-10T12:10:59Z","timestamp":1562760659000},"page":"419-420","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Towards evolutionary theorem proving for isabelle\/HOL"],"prefix":"10.1145","author":[{"given":"Yutaka","family":"Nagashima","sequence":"first","affiliation":[{"name":"University of Innsbruck, Czech Technical University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,7,13]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87827-8_28"},{"key":"e_1_3_2_1_2_1","unstructured":"Thomas C. Hales Mark Adams Gertrud Bauer Dat Tat Dang John Harrison Truong Le Hoang Cezary Kaliszyk Victor Magron Sean McLaughlin Thang Tat Nguyen Truong Quang Nguyen Tobias Nipkow Steven Obua Joseph Pleso Jason M. Rute Alexey Solovyev An Hoai Thi Ta Trung Nam Tran Diep Thi Trieu Josef Urban Ky Khac Vu and Roland Zumkeller. 2015. A formal proof of the Kepler conjecture. CoRR abs\/1501.02155 (2015). arXiv:1501.02155 http:\/\/arxiv.org\/abs\/1501.02155  Thomas C. Hales Mark Adams Gertrud Bauer Dat Tat Dang John Harrison Truong Le Hoang Cezary Kaliszyk Victor Magron Sean McLaughlin Thang Tat Nguyen Truong Quang Nguyen Tobias Nipkow Steven Obua Joseph Pleso Jason M. Rute Alexey Solovyev An Hoai Thi Ta Trung Nam Tran Diep Thi Trieu Josef Urban Ky Khac Vu and Roland Zumkeller. 2015. A formal proof of the Kepler conjecture. CoRR abs\/1501.02155 (2015). arXiv:1501.02155 http:\/\/arxiv.org\/abs\/1501.02155"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"key":"e_1_3_2_1_4_1","unstructured":"Gerwin Klein Tobias Nipkow Larry Paulson and Rene Thiemann. 2004. . https:\/\/www.isa-afp.org\/  Gerwin Klein Tobias Nipkow Larry Paulson and Rene Thiemann. 2004. . https:\/\/www.isa-afp.org\/"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"volume-title":"Towards Smart Proof Search for Isabelle. CoRR abs\/1701.03037","year":"2017","author":"Nagashima Yutaka","key":"e_1_3_2_1_7_1"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238210"},{"key":"e_1_3_2_1_9_1","volume-title":"Proceedings (Lecture Notes in Computer Science), Leonardo de Moura (Ed.)","volume":"10395","author":"Nagashima Yutaka","year":"2017"},{"key":"e_1_3_2_1_10_1","volume-title":"CICM 2018, Hagenberg, Austria, August 13--17, 2018, Proceedings (Lecture Notes in Computer Science), Florian Rabe, William M. Farmer, Grant O. Pass-more, and Abdou Youssef (Eds.)","volume":"11006","author":"Nagashima Yutaka","year":"2018"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9322-8"}],"event":{"name":"GECCO '19: Genetic and Evolutionary Computation Conference","sponsor":["SIGEVO ACM Special Interest Group on Genetic and Evolutionary Computation"],"location":"Prague Czech Republic","acronym":"GECCO '19"},"container-title":["Proceedings of the Genetic and Evolutionary Computation Conference Companion"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3319619.3321921","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3319619.3321921","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:54:34Z","timestamp":1750204474000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3319619.3321921"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,13]]},"references-count":11,"alternative-id":["10.1145\/3319619.3321921","10.1145\/3319619"],"URL":"https:\/\/doi.org\/10.1145\/3319619.3321921","relation":{},"subject":[],"published":{"date-parts":[[2019,7,13]]},"assertion":[{"value":"2019-07-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}