{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T04:10:31Z","timestamp":1748664631437,"version":"3.41.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319242453"},{"type":"electronic","value":"9783319242460"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24246-0_21","type":"book-chapter","created":{"date-parts":[[2015,9,19]],"date-time":"2015-09-19T04:20:53Z","timestamp":1442636453000},"page":"341-356","source":"Crossref","is-referenced-by-count":2,"title":["Lemmatization for Stronger Reasoning in Large Theories"],"prefix":"10.1007","author":[{"given":"Cezary","family":"Kaliszyk","sequence":"first","affiliation":[]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[]},{"given":"Ji\u0159\u00ed","family":"Vysko\u010dil","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,12]]},"reference":[{"issue":"2","key":"21_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\u00a052(2), 191\u2013213 (2014)","journal-title":"J. Autom. Reasoning"},{"doi-asserted-by":"crossref","unstructured":"Blanchette, J.C.: Redirecting proofs by contradiction. In: Blanchette, J.C., Urban, J. (eds.) PxTP@CADE. EPiC Series, vol.\u00a014, pp. 11\u201326. EasyChair (2013)","key":"21_CR2","DOI":"10.29007\/wm8b"},{"unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formalized Reasoning (in press, 2015)","key":"21_CR3"},{"key":"21_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1007\/3-540-45744-5_33","volume-title":"Automated Reasoning","author":"A. Fiedler","year":"2001","unstructured":"Fiedler, A.: P.rex: An interactive proof explainer. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 416\u2013420. Springer, Heidelberg (2001)"},{"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.\u00a014, pp. 87\u201395. EasyChair (2013)","key":"21_CR5","DOI":"10.29007\/5gzr"},{"issue":"2","key":"21_CR6","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-014-9303-3","volume":"53","author":"C. Kaliszyk","year":"2014","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. J. Autom. Reasoning\u00a053(2), 173\u2013213 (2014)","journal-title":"J. Autom. Reasoning"},{"key":"21_CR7","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/j.jsc.2014.09.032","volume":"69","author":"C. Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted theorem proving with millions of lemmas. Journal of Symbolic Computation\u00a069, 109\u2013128 (2015)","journal-title":"Journal of Symbolic Computation"},{"doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Urban, J.: MizAR 40 for Mizar 40. J. Automated Reasoning (in press, 2015)","key":"21_CR8","DOI":"10.1007\/s10817-015-9330-8"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-36675-8_8","volume-title":"Automated Reasoning and Mathematics","author":"M. Kinyon","year":"2013","unstructured":"Kinyon, M., Veroff, R., Vojt\u011bchovsk\u00fd, P.: Loops with abelian inner mapping groups: An application of automated deduction. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS, vol.\u00a07788, pp. 151\u2013164. Springer, Heidelberg (2013)"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L. Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 1\u201335. Springer, Heidelberg (2013)"},{"doi-asserted-by":"crossref","unstructured":"Kuehlwein, D., Urban, J.: Learning from multiple proofs: First experiments. In: Fontaine, P., Schmidt, R.A., Schulz, S. (eds.) PAAR 2012. EPiC Series, vol.\u00a021, pp. 82\u201394. EasyChair (2013)","key":"21_CR11","DOI":"10.29007\/nb2g"},{"key":"21_CR12","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.\u00a07998, pp. 35\u201350. Springer, Heidelberg (2013)"},{"key":"21_CR13","series-title":"LNCS(LNAI)","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/10721959_37","volume-title":"Automated Deduction - CADE-17","author":"A. Meier","year":"2000","unstructured":"Meier, A.: System description: Tramp: transformation of machine-found proofs into nd-proofs at the assertion level. In: McAllester, D. (ed.) CADE 2000. LNCS(LNAI), vol.\u00a01831, pp. 460\u2013464. Springer, Heidelberg (2000)"},{"unstructured":"Page, L., Brin, S., Motwani, R., Winograd, T.: The PageRank citation ranking: Bringing order to the Web. Technical report, Stanford Digital Library Technologies Project (1998)","key":"21_CR14"},{"issue":"2\u20133","key":"21_CR15","doi-asserted-by":"crossref","first-page":"267","DOI":"10.3233\/AIC-2010-0460","volume":"23","author":"J.D. Phillips","year":"2010","unstructured":"Phillips, J.D., Stanovsk\u00fd, D.: Automated theorem proving in quasigroup and loop theory. AI Commun.\u00a023(2\u20133), 267\u2013283 (2010)","journal-title":"AI Commun."},{"unstructured":"Puzis, Y., Gao, Y., Sutcliffe, G.: Automated generation of interesting theorems. In: Sutcliffe, G., Goebel, R. (eds.) FLAIRS, pp. 49\u201354. AAAI Press (2006)","key":"21_CR16"},{"unstructured":"Schulz, S.: Learning search control knowledge for equational deduction. DISKI, vol.\u00a0230. Infix Akademische Verlagsgesellschaft (2000)","key":"21_CR17"},{"key":"21_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"735","DOI":"10.1007\/978-3-642-45221-5_49","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S. Schulz","year":"2013","unstructured":"Schulz, S.: System description: E\u00a01.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol.\u00a08312, pp. 735\u2013743. Springer, Heidelberg (2013)"},{"doi-asserted-by":"crossref","unstructured":"Smolka, S.J., Blanchette, J.C.: Robust, semi-intelligible Isabelle proofs from ATP proofs. In: Blanchette, J.C., Urban, J. (eds.) PxTP 2013. EPiC Series, vol.\u00a014, pp. 117\u2013132. EasyChair (2013)","key":"21_CR19","DOI":"10.29007\/zbdb"},{"key":"21_CR20","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-540-73595-3_20","volume-title":"Automated Deduction \u2013 CADE-21","author":"G. Sutcliffe","year":"2007","unstructured":"Sutcliffe, G., Puzis, Y.: SRASS - A semantic relevance axiom selection system. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 295\u2013310. Springer, Heidelberg (2007)"},{"issue":"1","key":"21_CR21","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1142\/S0218213006002588","volume":"15","author":"J. Urban","year":"2006","unstructured":"Urban, J.: MoMM - fast interreduction and retrieval in large libraries of formalized mathematics. Int. J. on Artificial Intelligence Tools\u00a015(1), 109\u2013130 (2006)","journal-title":"Int. J. on Artificial Intelligence Tools"},{"unstructured":"Urban, J.: BliStr: The Blind Strategymaker. CoRR, abs\/1301.2683 (2014) (accepted to PAAR 2014)","key":"21_CR22"},{"issue":"2","key":"21_CR23","first-page":"231","volume":"2","author":"J. Urban","year":"2008","unstructured":"Urban, J., Sutcliffe, G.: ATP-based cross-verification of Mizar proofs: Method, systems, and first experiments. MCS\u00a02(2), 231\u2013251 (2008)","journal-title":"MCS"},{"doi-asserted-by":"crossref","unstructured":"Urban, J., Sutcliffe, G., Pudl\u00e1k, P., Vysko\u010dil, J.: MaLARea SG1 - machine learner for automated reasoning with semantic guidance. In: IJCAR, pp. 441\u2013456 (2008)","key":"21_CR24","DOI":"10.1007\/978-3-540-71070-7_37"},{"issue":"31","key":"21_CR25","first-page":"121","volume":"18","author":"J. Urban","year":"2009","unstructured":"Urban, J., Sutcliffe, G., Trac, S., Puzis, Y.: Combining mizar and TPTP semantic presentation and verification Tools. Studies in Logic, Grammar and Rhetoric\u00a018(31), 121\u2013136 (2009)","journal-title":"Studies in Logic, Grammar and Rhetoric"},{"issue":"3","key":"21_CR26","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. Reasoning\u00a016(3), 223\u2013239 (1996)","journal-title":"J. Autom. Reasoning"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24246-0_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T18:26:27Z","timestamp":1748629587000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24246-0_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319242453","9783319242460"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24246-0_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}