{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,12]],"date-time":"2026-11-12T17:10:21Z","timestamp":1794503421210,"version":"4.9.1"},"publisher-location":"Cham","reference-count":10,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319221014","type":"print"},{"value":"9783319221021","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-22102-1_15","type":"book-chapter","created":{"date-parts":[[2015,8,18]],"date-time":"2015-08-18T04:30:14Z","timestamp":1439872214000},"page":"227-233","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Learning to Parse on Aligned Corpora (Rough Diamond)"],"prefix":"10.1007","author":[{"given":"Cezary","family":"Kaliszyk","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ji\u0159\u00ed","family":"Vysko\u010dil","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,8,19]]},"reference":[{"key":"15_CR1","unstructured":"Blanchette, J. C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. Accepted to J. Formalized Reasoning (2015). Preprint at http:\/\/www4.in.tum.de\/~blanchet\/h4qed.pdf"},{"issue":"6","key":"15_CR2","first-page":"10","volume":"25","author":"EW Dijkstra","year":"1983","unstructured":"Dijkstra, E.W.: The fruits of misunderstanding. Elektronische Rechenanlagen 25(6), 10\u201313 (1983)","journal-title":"Elektronische Rechenanlagen"},{"key":"15_CR3","series-title":"London Mathematical Society Lecture Note Series","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139193894","volume-title":"Dense Sphere Packings: A Blueprint for Formal Proofs","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":"15_CR4","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"},{"issue":"1","key":"15_CR5","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s11786-014-0182-0","volume":"9","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: HOL(y)Hammer: online ATP service for HOL Light. Math. Comput. Sci. 9(1), 5\u201322 (2015)","journal-title":"Math. Comput. Sci."},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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, Heidelberg (2014)"},{"key":"15_CR7","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. 7364, pp. 378\u2013392. Springer, Heidelberg (2012)"},{"key":"15_CR8","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)"},{"issue":"2","key":"15_CR9","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$$\\,{\\hat{}}\\,\\,3$$. Inf. Control 10(2), 189\u2013208 (1967)","journal-title":"Inf. Control"},{"key":"15_CR10","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-22102-1_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T21:20:00Z","timestamp":1748553600000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-22102-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319221014","9783319221021"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-22102-1_15","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-319-22102-1","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"19 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}