{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,19]],"date-time":"2025-09-19T08:28:20Z","timestamp":1758270500218,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662488980"},{"type":"electronic","value":"9783662488997"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48899-7_7","type":"book-chapter","created":{"date-parts":[[2015,11,21]],"date-time":"2015-11-21T03:59:28Z","timestamp":1448078368000},"page":"88-96","source":"Crossref","is-referenced-by-count":25,"title":["FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover"],"prefix":"10.1007","author":[{"given":"Cezary","family":"Kaliszyk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"issue":"2","key":"7_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. Reasoning 52(2), 191\u2013213 (2014)","journal-title":"J. Autom. Reasoning"},{"key":"7_CR2","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formalized Reasoning (2015, in press)"},{"key":"7_CR3","unstructured":"Carlson, A., Cumby, C., Rosen, J., Roth, D.: The SNoW learning architecture. Technical report UIUCDCS-R-99-2101, UIUC Computer Science (1999)"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/978-3-319-08434-3_20","volume-title":"Intelligent Computer Mathematics","author":"T Gauthier","year":"2014","unstructured":"Gauthier, T., Kaliszyk, C.: Matching concepts across HOL libraries. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS, vol. 8543, pp. 267\u2013281. Springer, Heidelberg (2014)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/BFb0027415","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"O Ibens","year":"1997","unstructured":"Ibens, O., Letz, R.: Subgoal alternation in model elimination. In: Galmiche, D. (ed.) TABLEAUX 1997. LNCS, vol. 1227, pp. 201\u2013215. Springer, Heidelberg (1997)"},{"key":"7_CR6","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1108\/eb026526","volume":"28","author":"KS Jones","year":"1972","unstructured":"Jones, K.S.: A statistical interpretation of term specificity and its application in retrieval. J. Documentation 28, 11\u201321 (1972)","journal-title":"J. Documentation"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Urban, J.: Stronger automation for Flyspeck by feature weighting and strategy evolution. In: Blanchette, J.C., Urban, J. (eds.) PxTP 2013. EPiC Series, vol. 14, pp. 87\u201395. EasyChair (2013)","DOI":"10.29007\/5gzr"},{"key":"7_CR8","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s10817-015-9330-8","volume":"55","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: MizAR 40 for Mizar 40. J. Autom. Reasoning 55, 245\u2013256 (2015)","journal-title":"J. Autom. Reasoning"},{"key":"7_CR9","unstructured":"Kaliszyk, C., Urban, J., Vyskocil, J.: Efficient semantic features for automated reasoning over large theories. In: Yang, Q., Wooldridge, M. (eds.) IJCAI 2015, pp. 3084\u20133090. AAAI Press (2015)"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J.: Certified connection tableaux proofs for HOL Light and TPTP. In: Leroy, X., Tiu, A. (eds.) Proceedings of the 4th Conference on Certified Programs and Proofs (CPP 2015), pp. 59\u201366. ACM (2015)","DOI":"10.1145\/2676724.2693176"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-39634-2_6","volume-title":"Interactive Theorem Proving","author":"D K\u00fchlwein","year":"2013","unstructured":"K\u00fchlwein, D., Blanchette, J.C., Kaliszyk, C., Urban, J.: MaSh: machine learning for Sledgehammer. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 35\u201350. Springer, Heidelberg (2013)"},{"issue":"2\u20133","key":"7_CR12","doi-asserted-by":"crossref","first-page":"159","DOI":"10.3233\/AIC-2010-0464","volume":"23","author":"J Otten","year":"2010","unstructured":"Otten, J.: Restricting backtracking in connection calculi. AI Commun. 23(2\u20133), 159\u2013182 (2010)","journal-title":"AI Commun."},{"issue":"1\u20132","key":"7_CR13","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/S0747-7171(03)00037-3","volume":"36","author":"J Otten","year":"2003","unstructured":"Otten, J., Bibel, W.: leanCoP: lean connection-based theorem proving. J. Symb. Comput. 36(1\u20132), 139\u2013161 (2003)","journal-title":"J. Symb. Comput."},{"key":"7_CR14","unstructured":"Schulz, S.: Learning Search Control Knowledge for Equational Deduction. DISKI, vol. 230. Infix Akademische Verlagsgesellschaft (2000)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-15582-6_30","volume-title":"Mathematical Software \u2013 ICMS 2010","author":"J Urban","year":"2010","unstructured":"Urban, J., Hoder, K., Voronkov, A.: Evaluation of automated theorem proving on the Mizar Mathematical Library. In: Fukuda, K., Hoeven, J., Joswig, M., Takayama, N. (eds.) ICMS 2010. LNCS, vol. 6327, pp. 155\u2013166. Springer, Heidelberg (2010)"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-22119-4_21","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"J Urban","year":"2011","unstructured":"Urban, J., Vysko\u010dil, J., \u0160t\u011bp\u00e1nek, P.: MaLeCoP: Machine Learning Connection Prover. In: Br\u00fcnnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS, vol. 6793, pp. 263\u2013277. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48899-7_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T13:28:13Z","timestamp":1748698093000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48899-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662488980","9783662488997"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48899-7_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}