{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:15:17Z","timestamp":1775873717214,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642396335","type":"print"},{"value":"9783642396342","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39634-2_6","type":"book-chapter","created":{"date-parts":[[2013,7,22]],"date-time":"2013-07-22T09:52:36Z","timestamp":1374486756000},"page":"35-50","source":"Crossref","is-referenced-by-count":37,"title":["MaSh: Machine Learning for Sledgehammer"],"prefix":"10.1007","author":[{"given":"Daniel","family":"K\u00fchlwein","sequence":"first","affiliation":[]},{"given":"Jasmin Christian","family":"Blanchette","sequence":"additional","affiliation":[]},{"given":"Cezary","family":"Kaliszyk","sequence":"additional","affiliation":[]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","unstructured":"The Mizar Mathematical Library, http:\/\/mizar.org\/"},{"key":"6_CR2","doi-asserted-by":"crossref","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, http:\/\/arxiv.org\/abs\/1108.3446 (April 2013)","DOI":"10.1007\/s10817-013-9286-5"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-642-28717-6_6","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Alama","year":"2012","unstructured":"Alama, J., K\u00fchlwein, D., Urban, J.: Automated and human proofs in general mathematics: An initial comparison. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol.\u00a07180, pp. 37\u201345. Springer, Heidelberg (2012)"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"key":"6_CR5","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-71070-7_14","volume-title":"Automated Reasoning","author":"C. Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II\u2014A cooperative automatic theorem prover for higher-order logic (System description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 162\u2013170. Springer, Heidelberg (2008)"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/3-540-44659-1_3","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Berghofer","year":"2000","unstructured":"Berghofer, S., Nipkow, T.: Proof terms for simply typed higher order logic. In: Aagaard, M., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 38\u201352. Springer, Heidelberg (2000)"},{"issue":"1","key":"6_CR7","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10817-013-9278-5","volume":"51","author":"J.C. Blanchette","year":"2013","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J. Autom. Reasoning\u00a051(1), 109\u2013128 (2013), http:\/\/www21.in.tum.de\/~blanchet\/jar-smt.pdf","journal-title":"J. Autom. Reasoning"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/978-3-642-36742-7_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.C. Blanchette","year":"2013","unstructured":"Blanchette, J.C., B\u00f6hme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: Piterman, N., Smolka, S. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 493\u2013507. Springer, Heidelberg (2013)"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-642-32347-8_24","volume-title":"Interactive Theorem Proving","author":"J.C. Blanchette","year":"2012","unstructured":"Blanchette, J.C., Popescu, A., Wand, D., Weidenbach, C.: More SPASS with Isabelle\u2014Superposition with hard sorts and configurable simplification. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 345\u2013360. Springer, Heidelberg (2012)"},{"key":"6_CR10","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-14203-1_9","volume-title":"Automated Reasoning","author":"S. B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: Judgement Day. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol.\u00a06173, pp. 107\u2013121. Springer, Heidelberg (2010)"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-31365-3_11","volume-title":"Automated Reasoning","author":"C.E. Brown","year":"2012","unstructured":"Brown, C.E.: Satallax: An automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 111\u2013117. Springer, Heidelberg (2012)"},{"key":"6_CR12","unstructured":"Carlson, A.J., Cumby, C.M., Rosen, J.L., Roth, D.: SNoW user guide. Tech. rep., C.S. Dept., University of Illinois at Urbana-Champaign (1999), http:\/\/cogcomp.cs.illinois.edu\/papers\/CCRR99.pdf"},{"key":"6_CR13","unstructured":"Dutertre, B., de Moura, L.: The Yices SMT solver (2006), http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"key":"6_CR14","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-642-22438-6_23","volume-title":"Automated Deduction \u2013 CADE-23","author":"K. Hoder","year":"2011","unstructured":"Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol.\u00a06803, pp. 299\u2013314. Springer, Heidelberg (2011)"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-22863-6_12","volume-title":"Interactive Theorem Proving","author":"J. H\u00f6lzl","year":"2011","unstructured":"H\u00f6lzl, J., Heller, A.: Three chapters of measure theory in Isabelle\/HOL. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 135\u2013151. Springer, Heidelberg (2011)"},{"key":"6_CR16","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Di Vito, B., Mu\u00f1oz, C. (eds.) Design and Application of Strategies\/Tactics in Higher Order Logics, pp. 56\u201368. NASA Tech. Reports (2003)"},{"key":"6_CR17","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. CoRR abs\/1211.7012 (2012), http:\/\/arxiv.org\/abs\/1211.7012"},{"key":"6_CR18","unstructured":"Klein, G., Nipkow, T.: Jinja is not Java. In: Klein, G., Nipkow, T., Paulson, L. (eds.) Archive of Formal Proofs (2005), http:\/\/afp.sf.net\/entries\/Jinja.shtml"},{"key":"6_CR19","unstructured":"Klein, G., Nipkow, T., Paulson, L. (eds.): Archive of Formal Proofs, http:\/\/afp.sf.net\/"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-642-31365-3_30","volume-title":"Automated Reasoning","author":"D. K\u00fchlwein","year":"2012","unstructured":"K\u00fchlwein, D., van Laarhoven, T., Tsivtsivadze, E., Urban, J., Heskes, T.: Overview and evaluation of premise selection techniques for large theory mathematics. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 378\u2013392. Springer, Heidelberg (2012)"},{"key":"6_CR21","unstructured":"K\u00fchlwein, D., Urban, J.: Learning from multiple proofs: First experiments. In: Fontaine, P., Schmidt, R., Schulz, S. (eds.) PAAR-2012, pp. 82\u201394 (2012)"},{"issue":"1","key":"6_CR22","first-page":"3","volume":"4","author":"R. Matuszewski","year":"2005","unstructured":"Matuszewski, R., Rudnicki, P.: Mizar: The first 30 years. Mechanized Mathematics and Its Applications\u00a04(1), 3\u201324 (2005)","journal-title":"Mechanized Mathematics and Its Applications"},{"issue":"1","key":"6_CR23","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.jal.2007.07.004","volume":"7","author":"J. Meng","year":"2009","unstructured":"Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Applied Logic\u00a07(1), 41\u201357 (2009)","journal-title":"J. Applied Logic"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"issue":"1-2","key":"6_CR26","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L.C. Paulson","year":"1998","unstructured":"Paulson, L.C.: The inductive approach to verifying cryptographic protocols. J. Comput. Secur.\u00a06(1-2), 85\u2013128 (1998)","journal-title":"J. Comput. Secur."},{"key":"6_CR27","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, A practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Ternovska, E., Schulz, S. (eds.) IWIL-2010 (2010)"},{"issue":"2-3","key":"6_CR28","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Comm.\u00a015(2-3), 91\u2013110 (2002)","journal-title":"AI Comm."},{"key":"6_CR29","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-25984-8_15","volume-title":"Automated Reasoning","author":"S. Schulz","year":"2004","unstructured":"Schulz, S.: System description: E\u00a00.81. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 223\u2013228. Springer, Heidelberg (2004)"},{"key":"6_CR30","unstructured":"Schulz, S.: First-order deduction for large knowledge bases. Presentation at Deduction at Scale 2011 Seminar, Ringberg Castle (2011), http:\/\/www.mpi-inf.mpg.de\/departments\/rg1\/conferences\/deduction10\/slides\/stephan-schulz.pdf"},{"issue":"2","key":"6_CR31","doi-asserted-by":"crossref","first-page":"211","DOI":"10.3233\/AIC-130550","volume":"26","author":"G. Sutcliffe","year":"2013","unstructured":"Sutcliffe, G.: The 6th IJCAR automated theorem proving system competition\u2014CASC-J6. AI Commun.\u00a026(2), 211\u2013223 (2013)","journal-title":"AI Commun."},{"issue":"1","key":"6_CR32","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1142\/S0218213006002588","volume":"15","author":"J. Urban","year":"2006","unstructured":"Urban, J.: MoMM\u2014Fast interreduction and retrieval in large libraries of formalized mathematics. Int. J. AI Tools\u00a015(1), 109\u2013130 (2006)","journal-title":"Int. J. AI Tools"},{"issue":"1-2","key":"6_CR33","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s10817-006-9032-3","volume":"37","author":"J. Urban","year":"2006","unstructured":"Urban, J.: MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning\u00a037(1-2), 21\u201343 (2006)","journal-title":"J. Autom. Reasoning"},{"key":"6_CR34","unstructured":"Urban, J.: MaLARea: A metasystem for automated reasoning in large theories. In: Sutcliffe, G., Urban, J., Schulz, S. (eds.) ESARLT 2007. CEUR Workshop Proceedings, vol.\u00a0257. CEUR-WS.org (2007)"},{"key":"6_CR35","unstructured":"Urban, J.: An overview of methods for large-theory automated theorem proving. In: H\u00f6fner, P., McIver, A., Struth, G. (eds.) ATE-2011. CEUR Workshop Proceedings, vol.\u00a0760, pp. 3\u20138. CEUR-WS.org (2011)"},{"key":"6_CR36","unstructured":"Urban, J.: BliStr: The blind strategymaker. CoRR abs\/1301.2683 (2013), http:\/\/arxiv.org\/abs\/1301.2683"},{"issue":"2","key":"6_CR37","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10817-012-9269-y","volume":"50","author":"J. Urban","year":"2013","unstructured":"Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. J. Autom. Reasoning\u00a050(2), 229\u2013241 (2013)","journal-title":"J. Autom. Reasoning"},{"key":"6_CR38","series-title":"LNAI","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\u2014 Machine learner for automated reasoning with semantic guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 441\u2013456. Springer, Heidelberg (2008)"},{"key":"6_CR39","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-642-36675-8_13","volume-title":"Automated Reasoning and Mathematics","author":"J. Urban","year":"2013","unstructured":"Urban, J., Vysko\u010dil, J.: Theorem proving in large formal mathematics as an emerging AI field. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS (LNAI), vol.\u00a07788, pp. 240\u2013257. Springer, Heidelberg (2013)"},{"key":"6_CR40","unstructured":"Wenzel, M.: Isabelle\/Isar\u2014A generic framework for human-readable proof documents. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof\u2014Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar, and Rhetoric, vol.\u00a010(23). Uniwersytet w Bia\u0142ymstoku (2007)"},{"key":"6_CR41","unstructured":"Wenzel, M.: Parallel proof checking in Isabelle\/Isar. In: Dos Reis, G., Th\u00e9ry, L. (eds.) PLMMS 2009, pp. 13\u201329. ACM Digital Library (2009)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39634-2_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,31]],"date-time":"2020-07-31T07:19:59Z","timestamp":1596179999000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39634-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642396335","9783642396342"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39634-2_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}