{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T01:28:45Z","timestamp":1784770125889,"version":"3.55.0"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,4,24]],"date-time":"2013-04-24T00:00:00Z","timestamp":1366761600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2014,2]]},"DOI":"10.1007\/s10817-013-9286-5","type":"journal-article","created":{"date-parts":[[2013,4,23]],"date-time":"2013-04-23T08:08:28Z","timestamp":1366704508000},"page":"191-213","source":"Crossref","is-referenced-by-count":69,"title":["Premise Selection for Mathematics by Corpus Analysis and Kernel Methods"],"prefix":"10.1007","volume":"52","author":[{"given":"Jesse","family":"Alama","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tom","family":"Heskes","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniel","family":"K\u00fchlwein","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Evgeni","family":"Tsivtsivadze","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2013,4,24]]},"reference":[{"key":"9286_CR1","unstructured":"Alama, J.: Formal proofs and refutations. Ph.D. thesis, Stanford University (2009)"},{"key":"9286_CR2","doi-asserted-by":"crossref","unstructured":"Alama, J., Brink, K., Mamane, L., Urban, J.: Large formal wikis: Issues and solutions. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus\/MKM. Lecture Notes in Computer Science, vol.\u00a06824, pp.\u00a0133\u2013148. Springer (2011)","DOI":"10.1007\/978-3-642-22673-1_10"},{"key":"9286_CR3","doi-asserted-by":"crossref","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. Lecture Notes in Computer Science, vol.\u00a07180, pp.\u00a037\u201345. Springer (2012)","DOI":"10.1007\/978-3-642-28717-6_6"},{"key":"9286_CR4","doi-asserted-by":"crossref","unstructured":"Alama, J., Mamane, L., Urban, J.: Dependencies in formal mathematics: applications and extraction for Coq and Mizar. In: Jeuring, J., Campbell, J.A., Carette, J., Reis, G.D., Sojka, P., Wenzel, M., Sorge, V. (eds.) AISC\/MKM\/Calculemus. Lecture Notes in Computer Science, vol.\u00a07362, pp.\u00a01\u201316. Springer (2012)","DOI":"10.1007\/978-3-642-31374-5_1"},{"key":"9286_CR5","doi-asserted-by":"crossref","unstructured":"Aronszajn, N.: Theory of reproducing kernels. Trans. Am. Math. Soc. 68, 337\u2013404 (1950)","DOI":"10.1090\/S0002-9947-1950-0051437-7"},{"key":"9286_CR6","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development. Coq\u2019Art: the calculus of inductive constructions. In: Texts in Theoretical Computer Science. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"9286_CR7","volume-title":"Pattern Recognition and Machine Learning (Information Science and Statistics)","author":"CM Bishop","year":"2006","unstructured":"Bishop, C.M.: Pattern Recognition and Machine Learning (Information Science and Statistics). Springer, Secaucus (2006)"},{"key":"9286_CR8","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle\/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCos. Lecture Notes in Computer Science, vol.\u00a06989, pp.\u00a012\u201327. Springer (2011)","DOI":"10.1007\/978-3-642-24364-6_2"},{"key":"9286_CR9","unstructured":"Carlson, A., Cumby, C., Rosen, J., Roth, D.: The SNoW learning architecture. Tech. Rep. UIUCDCS-R-99-2101, UIUC Computer Science Department (1999). http:\/\/cogcomp.cs.illinois.edu\/papers\/CCRR99.pdf"},{"key":"9286_CR10","unstructured":"Davis, M.: Obvious logical inferences. In: Hayes, P.J. (ed.) IJCAI, pp.\u00a0530\u2013531. Kaufmann (1981)"},{"issue":"2","key":"9286_CR11","first-page":"153","volume":"3","author":"A Grabowski","year":"2010","unstructured":"Grabowski, A., Korni\u0142owicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formaliz. Reason. 3(2), 153\u2013245 (2010)","journal-title":"J. Formaliz. Reason."},{"key":"9286_CR12","doi-asserted-by":"crossref","unstructured":"Harrison, J.: HOL light: A tutorial introduction. In: Srivas, M.K., Camilleri, A.J. (eds.) FMCAD. Lecture Notes in Computer Science, vol.\u00a01166, pp.\u00a0265\u2013269. Springer (1996)","DOI":"10.1007\/BFb0031814"},{"key":"9286_CR13","doi-asserted-by":"crossref","unstructured":"Harrison, J., Slind, K., Arthan, R.: HOL. In: Wiedijk, F. (ed.) The Seventeen Provers of the World. Lecture Notes in Computer Science, vol.\u00a03600, pp.\u00a011\u201319. Springer (2006)","DOI":"10.1007\/11542384_3"},{"key":"9286_CR14","doi-asserted-by":"crossref","unstructured":"Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE. Lecture Notes in Computer Science, vol.\u00a06803, pp.\u00a0299\u2013314. Springer (2011)","DOI":"10.1007\/978-3-642-22438-6_23"},{"issue":"1","key":"9286_CR15","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/s10817-007-9085-y","volume":"40","author":"J Meng","year":"2008","unstructured":"Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reason. 40(1), 35\u201360 (2008)","journal-title":"J. Autom. Reason."},{"key":"9286_CR16","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS. Lecture Notes in Computer Science, vol.\u00a04963, pp.\u00a0337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9286_CR17","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014A proof assistant for higher-order logic. Lecture Notes in Computer Science, vol.\u00a02283. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"9286_CR18","doi-asserted-by":"crossref","unstructured":"Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) TPHOLs. Lecture Notes in Computer Science, vol.\u00a04732, pp.\u00a0232\u2013245. Springer (2007)","DOI":"10.1007\/978-3-540-74591-4_18"},{"key":"9286_CR19","unstructured":"Pease, A., Sutcliffe, G.: First order reasoning on a large ontology. In: Sutcliffe, G., Urban, J., Schulz, S. (eds.) Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, Bremen, Germany, 17th July 2007. CEUR Workshop Proceedings, vol.\u00a0257. CEUR-WS.org (2007)"},{"issue":"2\u20133","key":"9286_CR20","first-page":"91","volume":"15","author":"A Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun. 15(2\u20133), 91\u2013110 (2002)","journal-title":"AI Commun."},{"issue":"4","key":"9286_CR21","doi-asserted-by":"crossref","first-page":"461","DOI":"10.1162\/neco.1991.3.4.461","volume":"3","author":"MD Richard","year":"2010","unstructured":"Richard, M.D., Lippmann, R.P.: Neural network classifiers estimate Bayesian a posteriori probabilities. Neural Comput. 3(4), 461\u2013483 (2010)","journal-title":"Neural Comput."},{"key":"9286_CR22","first-page":"131","volume-title":"Advances in Learning Theory: Methods, Model and Applications","author":"R Rifkin","year":"2003","unstructured":"Rifkin, R., Yeo, G., Poggio, T.: Regularized least-squares classification. In: Suykens, J., Horvath, G., Basu, S., Micchelli, C., Vandewalle, J. (eds.) Advances in Learning Theory: Methods, Model and Applications, pp.\u00a0131\u2013154. IOS Press, Amsterdam (2003)"},{"issue":"4","key":"9286_CR23","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1007\/BF00247436","volume":"3","author":"P Rudnicki","year":"1987","unstructured":"Rudnicki, P.: Obvious inferences. J. Autom. Reason. 3(4), 383\u2013393 (1987)","journal-title":"J. Autom. Reason."},{"key":"9286_CR24","doi-asserted-by":"crossref","unstructured":"Schoelkopf, B., Herbrich, R., Williamson, R., Smola, A.J.: A generalized representer theorem. In: Helmbold, D., Williamson, R. (eds.) Proceedings of the 14th Annual Conference on Computational Learning Theory, pp.\u00a0416\u2013426. Berlin, Germany (2001)","DOI":"10.1007\/3-540-44581-1_27"},{"key":"9286_CR25","volume-title":"Learning with Kernels: Support Vector Machines, Regularization, Optimization, and Beyond","author":"B Scholkopf","year":"2001","unstructured":"Scholkopf, B., Smola, A.J.: Learning with Kernels: Support Vector Machines, Regularization, Optimization, and Beyond. MIT Press, Cambridge (2001)"},{"issue":"2\u20133","key":"9286_CR26","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."},{"issue":"1","key":"9286_CR27","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10107-010-0420-4","volume":"127","author":"S Shalev-Shwartz","year":"2011","unstructured":"Shalev-Shwartz, S., Singer, Y., Srebro, N., Cotter, A.: Pegasos: primal estimated sub-gradient solver for SVM. Math. Program. 127(1), 3\u201330 (2011)","journal-title":"Math. Program."},{"key":"9286_CR28","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511809682","volume-title":"Kernel Methods for Pattern Analysis","author":"J Shawe-Taylor","year":"2004","unstructured":"Shawe-Taylor, J., Cristianini, N.: Kernel Methods for Pattern Analysis. Cambridge University Press, New York (2004)"},{"key":"9286_CR29","doi-asserted-by":"crossref","unstructured":"Simpson, S.G.: Subsystems of Second Order Arithmetic, 2nd edn. Perspectives in Mathematical Logic. Springer (2009)","DOI":"10.1017\/CBO9780511581007"},{"key":"9286_CR30","unstructured":"Solovay, R.: AC and strongly inaccessible cardinals. Available on the Foundations of Mathematics archives at http:\/\/www.cs.nyu.edu\/pipermail\/fom\/2008-March\/012783.html (2008)"},{"key":"9286_CR31","doi-asserted-by":"crossref","first-page":"176","DOI":"10.4064\/fm-32-1-176-783","volume":"32","author":"A Tarski","year":"1939","unstructured":"Tarski, A.: On well-ordered subsets of any set. Fundam. Math. 32, 176\u2013183 (1939)","journal-title":"Fundam. Math."},{"issue":"1","key":"9286_CR32","first-page":"9","volume":"1","author":"A Trybulec","year":"1990","unstructured":"Trybulec, A.: Tarski Grothendieck set theory. Formaliz. Math. 1(1), 9\u201311 (1990)","journal-title":"Formaliz. Math."},{"key":"9286_CR33","first-page":"107","volume-title":"Preference Learning","author":"E Tsivtsivadze","year":"2011","unstructured":"Tsivtsivadze, E., Pahikkala, T., Boberg, J., Salakoski, T., Heskes, T.: Co-regularized least-squares for label ranking. In: F\u00fcrnkranz, J., H\u00fcllermeier, E. (eds.) Preference Learning, pp.\u00a0107\u2013123. Springer, Berlin (2011)"},{"issue":"3\u20134","key":"9286_CR34","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/s10817-004-6245-1","volume":"33","author":"J Urban","year":"2004","unstructured":"Urban, J.: MPTP\u2014motivation, implementation, first experiments. J. Autom. Reason. 33(3\u20134), 319\u2013339 (2004)","journal-title":"J. Autom. Reason."},{"issue":"1\u20132","key":"9286_CR35","first-page":"21","volume":"37","author":"J Urban","year":"2006","unstructured":"Urban, J.: MPTP 0.2: design, implementation, and initial experiments. J. Autom. Reason. 37(1\u20132), 21\u201343 (2006)","journal-title":"J. Autom. Reason."},{"key":"9286_CR36","doi-asserted-by":"crossref","unstructured":"Urban, J., Hoder, K., Voronkov, A.: Evaluation of automated theorem proving on the Mizar Mathematical Library. In: Fukuda, K., van\u00a0der Hoeven, J., Joswig, M., Takayama, N. (eds.) ICMS. Lecture Notes in Computer Science, vol.\u00a06327, pp.\u00a0155\u2013166. Springer (2010)","DOI":"10.1007\/978-3-642-15582-6_30"},{"key":"9286_CR37","doi-asserted-by":"crossref","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. Reason. 50, 229\u2013241 (2013)","journal-title":"J. Autom. Reason."},{"key":"9286_CR38","unstructured":"Urban, J., Sutcliffe, G.: Automated reasoning and presentation support for formalizing mathematics in Mizar. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC\/MKM\/Calculemus. Lecture Notes in Computer Science, vol.\u00a06167, pp.\u00a0132\u2013146. Springer (2010)"},{"key":"9286_CR39","doi-asserted-by":"crossref","unstructured":"Urban, J., Sutcliffe, G., Pudl\u00e1k, P., Vyskocil, J.: MaLARea SG1- machine learner for automated reasoning with semantic guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR. Lecture Notes in Computer Science, vol.\u00a05195, pp.\u00a0441\u2013456. Springer (2008)","DOI":"10.1007\/978-3-540-71070-7_37"},{"key":"9286_CR40","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE. LNCS, vol.\u00a05663, pp.\u00a0140\u2013145. Springer (2009)","DOI":"10.1007\/978-3-642-02959-2_10"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9286-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-013-9286-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9286-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T23:24:02Z","timestamp":1562973842000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-013-9286-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,4,24]]},"references-count":40,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,2]]}},"alternative-id":["9286"],"URL":"https:\/\/doi.org\/10.1007\/s10817-013-9286-5","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,4,24]]}}}