{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T16:03:37Z","timestamp":1725984217138},"publisher-location":"Cham","reference-count":9,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319968117"},{"type":"electronic","value":"9783319968124"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-96812-4_11","type":"book-chapter","created":{"date-parts":[[2018,7,17]],"date-time":"2018-07-17T08:26:41Z","timestamp":1531816001000},"page":"118-124","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Enhancing ENIGMA Given Clause Guidance"],"prefix":"10.1007","author":[{"given":"Jan","family":"Jakub\u016fv","sequence":"first","affiliation":[]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"issue":"2","key":"11_CR1","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10817-013-9286-5","volume":"52","author":"J Alama","year":"2014","unstructured":"Alama, J., Heskes, T., K\u00fchlwein, D., Tsivtsivadze, E., Urban, J.: Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reason. 52(2), 191\u2013213 (2014). \nhttps:\/\/doi.org\/10.1007\/s10817-013-9286-5","journal-title":"J. Autom. Reason."},{"key":"11_CR2","first-page":"1871","volume":"9","author":"R Fan","year":"2008","unstructured":"Fan, R., Chang, K., Hsieh, C., Wang, X., Lin, C.: LIBLINEAR: a library for large linear classification. J. Mach. Learn. Res. 9, 1871\u20131874 (2008)","journal-title":"J. Mach. Learn. Res."},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-319-42547-4_11","volume-title":"Intelligent Computer Mathematics","author":"J Jakub\u016fv","year":"2016","unstructured":"Jakub\u016fv, J., Urban, J.: Extending E prover with similarity based clause selection strategies. In: Kohlhase, M., Johansson, M., Miller, B., de de Moura, L., Tompa, F. (eds.) CICM 2016. LNCS (LNAI), vol. 9791, pp. 151\u2013156. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-42547-4_11"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-319-62075-6_20","volume-title":"Intelligent Computer Mathematics","author":"J Jakub\u016fv","year":"2017","unstructured":"Jakub\u016fv, J., Urban, J.: ENIGMA: efficient learning-based inference guiding machine. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS (LNAI), vol. 10383, pp. 292\u2013302. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-62075-6_20"},{"issue":"2\u20133","key":"11_CR5","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E - a brainiac theorem prover. AI Commun. 15(2\u20133), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-642-36675-8_3","volume-title":"Automated Reasoning and Mathematics","author":"S Schulz","year":"2013","unstructured":"Schulz, S.: Simple and efficient clause subsumption with feature vector indexing. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS (LNAI), vol. 7788, pp. 45\u201367. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-36675-8_3"},{"issue":"5","key":"11_CR7","doi-asserted-by":"publisher","first-page":"607","DOI":"10.3233\/AIC-160709","volume":"29","author":"G Sutcliffe","year":"2016","unstructured":"Sutcliffe, G.: The 8th IJCAR automated theorem proving system competition - CASC-J8. AI Commun. 29(5), 607\u2013619 (2016). \nhttps:\/\/doi.org\/10.3233\/AIC-160709","journal-title":"AI Commun."},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-540-71070-7_37","volume-title":"Automated Reasoning","author":"J Urban","year":"2008","unstructured":"Urban, J., Sutcliffe, G., Pudl\u00e1k, P., Vysko\u010dil, J.: MaLARea SG1 - machine learner for automated reasoning with semantic guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 441\u2013456. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71070-7_37"},{"issue":"3","key":"11_CR9","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/BF00252178","volume":"16","author":"R Veroff","year":"1996","unstructured":"Veroff, R.: Using hints to increase the effectiveness of an automated reasoning program: case studies. J. Autom. Reason. 16(3), 223\u2013239 (1996). \nhttps:\/\/doi.org\/10.1007\/BF00252178","journal-title":"J. Autom. Reason."}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96812-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,7,17]],"date-time":"2018-07-17T08:30:56Z","timestamp":1531816256000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96812-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319968117","9783319968124"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96812-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}