{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:48Z","timestamp":1774837848020,"version":"3.50.1"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319661063","type":"print"},{"value":"9783319661070","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66107-0_2","type":"book-chapter","created":{"date-parts":[[2017,8,20]],"date-time":"2017-08-20T14:13:59Z","timestamp":1503238439000},"page":"12-27","source":"Crossref","is-referenced-by-count":13,"title":["Automating Formalization by Statistical and Semantic Parsing of Mathematics"],"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","reference":[{"issue":"3\u20134","key":"2_CR1","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1023\/A:1021966832558","volume":"29","author":"G Bancerek","year":"2002","unstructured":"Bancerek, G., Rudnicki, P.: A compendium of continuous lattices in MIZAR. J. Autom. Reason. 29(3\u20134), 189\u2013224 (2002)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"2_CR2","first-page":"101","volume":"9","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formaliz. Reason. 9(1), 101\u2013148 (2016)","journal-title":"J. Formaliz. Reason."},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Collins, M.: Three generative, lexicalised models for statistical parsing. In: Cohen, P.R., Wahlster, W. (eds.) Proceedings of the 35th Annual Meeting of the Association for Computational Linguistics and 8th Conference of the European Chapter of the Association for Computational Linguistics, pp. 16\u201323. Morgan Kaufmann Publishers\/ACL (1997)","DOI":"10.3115\/976909.979620"},{"key":"2_CR4","unstructured":"The Coq Proof Assistant. http:\/\/coq.inria.fr"},{"issue":"6","key":"2_CR5","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1002\/(SICI)1097-4571(199009)41:6<391::AID-ASI1>3.0.CO;2-9","volume":"41","author":"SC Deerwester","year":"1990","unstructured":"Deerwester, S.C., Dumais, S.T., Landauer, T.K., Furnas, G.W., Harshman, R.A.: Indexing by latent semantic analysis. JASIS 41(6), 391\u2013407 (1990)","journal-title":"JASIS"},{"issue":"4","key":"2_CR6","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1109\/TSMC.1976.5408784","volume":"6","author":"SA Dudani","year":"1976","unstructured":"Dudani, S.A.: The distance-weighted K-nearest-neighbor rule. IEEE Trans. Syst. Man Cybern. 6(4), 325\u2013327 (1976)","journal-title":"IEEE Trans. Syst. Man Cybern."},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-03359-9_23","volume-title":"Theorem Proving in Higher Order Logics","author":"F Garillot","year":"2009","unstructured":"Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 327\u2013342. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-03359-9_23"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Cham (2014). doi:10.1007\/978-3-319-08434-3_20"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-39634-2_14","volume-title":"Interactive Theorem Proving","author":"G Gonthier","year":"2013","unstructured":"Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 163\u2013179. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39634-2_14"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-642-32347-8_25","volume-title":"Interactive Theorem Proving","author":"G Gonthier","year":"2012","unstructured":"Gonthier, G., Tassi, E.: A language of patterns for subterm selection. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 361\u2013376. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-32347-8_25"},{"issue":"2","key":"2_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":"2_CR12","unstructured":"Greenbaum, S.: Input transformations and resolution implementation techniques for theorem-proving in first-order logic. Ph.D. thesis, University of Illinois at Urbana-Champaign (1986)"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-540-74464-1_11","volume-title":"Types for Proofs and Programs","author":"F Haftmann","year":"2007","unstructured":"Haftmann, F., Wenzel, M.: Constructive type classes in isabelle. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 160\u2013174. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-74464-1_11"},{"key":"2_CR14","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139193894","volume-title":"Dense Sphere Packings a Blueprint for Formal Proofs, London Mathematical Society Lecture Note Series","author":"T Hales","year":"2012","unstructured":"Hales, T.: Dense Sphere Packings a Blueprint for Formal Proofs, London Mathematical Society Lecture Note Series, vol. 400. Cambridge University Press, Cambridge (2012)"},{"key":"2_CR15","unstructured":"Hales, T.C., Adams, M., Bauer, G., Dang, D.T., Harrison, J., Hoang, T.L., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T.T., Nguyen, T.Q., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, A.H.T., Tran, T.N., Trieu, D.T., Urban, J., Vu, K.K., Zumkeller, R.: A formal proof of the Kepler conjecture. CoRR, abs\/1501.02155, 2015"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J Harrison","year":"1996","unstructured":"Harrison, J.: HOL Light: a tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265\u2013269. Springer, Heidelberg (1996). doi:10.1007\/BFb0031814"},{"key":"2_CR17","series-title":"Handbook of the History of Logic","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-444-51624-4.50004-6","volume-title":"Computational Logic","author":"J Harrison","year":"2014","unstructured":"Harrison, J., Urban, J., Wiedijk, F.: History of interactive theorem proving. In: Siekmann, J.H. (ed.) Computational Logic. Handbook of the History of Logic, vol. 9. Elsevier, Amsterdam (2014)"},{"issue":"2","key":"2_CR18","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. Reason. 53(2), 173\u2013213 (2014)","journal-title":"J. Autom. Reason."},{"key":"2_CR19","unstructured":"Kaliszyk, C., Urban, J., Vyskocil, J.: System description: statistical parsing of informalized Mizar formulas. http:\/\/grid01.ciirc.cvut.cz\/mptp\/synasc17sd.pdf"},{"key":"2_CR20","first-page":"3084","volume-title":"IJCAI 2015","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J.: Efficient semantic features for automated reasoning over large theories. In: Yang, Q., Wooldridge, M. (eds.) IJCAI 2015, pp. 3084\u20133090. AAAI Press, Menlo Park (2015)"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-319-22102-1_15","volume-title":"Interactive Theorem Proving","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J.: Learning to parse on aligned corpora (rough diamond). In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 227\u2013233. Springer, Cham (2015). doi:10.1007\/978-3-319-22102-1_15"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-3-319-08434-3_34","volume-title":"Intelligent Computer Mathematics","author":"C Kaliszyk","year":"2014","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J., Geuvers, H.: Developing corpus-based translation methods between informal and formal mathematics: project description. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS, vol. 8543, pp. 435\u2013439. Springer, Cham (2014). doi:10.1007\/978-3-319-08434-3_34"},{"issue":"6","key":"2_CR23","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1743546.1743574","volume":"53","author":"G Klein","year":"2010","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an operating-system kernel. Commun. ACM 53(6), 107\u2013115 (2010)","journal-title":"Commun. ACM"},{"key":"2_CR24","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. 8044, pp. 1\u201335. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39799-8_1"},{"key":"2_CR25","first-page":"1","volume":"8","author":"M Lange","year":"2009","unstructured":"Lange, M., Lei\u00df, H.: To CNF or not to CNF? an efficient yet presentable version of the CYK algorithm. Inform. Didact. 8, 1\u201321 (2009). https:\/\/www.informaticadidactica.de\/uploads\/Artikel\/LangeLeiss2009\/LangeLeiss2009.pdf","journal-title":"Inform. Didact."},{"issue":"7","key":"2_CR26","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"2_CR27","volume-title":"Handbook of Automated Reasoning (in 2 Volumes)","year":"2001","unstructured":"Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning (in 2 Volumes). Elsevier and MIT Press, Cambridge (2001)"},{"issue":"1\/2","key":"2_CR28","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1006\/jsco.2001.0456","volume":"32","author":"P Rudnicki","year":"2001","unstructured":"Rudnicki, P., Schwarzweller, C., Trybulec, A.: Commutative algebra in the Mizar system. J. Symb. Comput. 32(1\/2), 143\u2013169 (2001)","journal-title":"J. Symb. Comput."},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-642-39320-4_10","volume-title":"Intelligent Computer Mathematics","author":"C Tankink","year":"2013","unstructured":"Tankink, C., Kaliszyk, C., Urban, J., Geuvers, H.: Formal mathematics on display: a wiki for Flyspeck. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS, vol. 7961, pp. 152\u2013167. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39320-4_10"},{"key":"2_CR30","series-title":"Lecture Notes in Computer Science","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, vol. 7788, pp. 240\u2013257. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-36675-8_13"},{"key":"2_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-71067-7_7","volume-title":"Theorem Proving in Higher Order Logics","author":"M Wenzel","year":"2008","unstructured":"Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle framework. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 33\u201338. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-71067-7_7"},{"issue":"2","key":"2_CR32","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/S0019-9958(67)80007-X","volume":"10","author":"DH Younger","year":"1967","unstructured":"Younger, D.H.: Recognition and parsing of context-free languages in time $$n^{3}$$. Inf. Control 10(2), 189\u2013208 (1967)","journal-title":"Inf. Control"},{"key":"2_CR33","unstructured":"Zinn, C.: Understanding informal mathematical discourse. Ph.D. thesis, University of Erlangen-Nuremberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66107-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,29]],"date-time":"2022-09-29T06:05:08Z","timestamp":1664431508000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-66107-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661063","9783319661070"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66107-0_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}