{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T06:04:21Z","timestamp":1726034661274},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030232498"},{"type":"electronic","value":"9783030232504"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-23250-4_2","type":"book-chapter","created":{"date-parts":[[2019,7,2]],"date-time":"2019-07-02T03:01:17Z","timestamp":1562036477000},"page":"16-27","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Beginners\u2019 Quest to Formalize Mathematics: A Feasibility Study in Isabelle"],"prefix":"10.1007","author":[{"given":"Jonas","family":"Bayer","sequence":"first","affiliation":[]},{"given":"Marco","family":"David","sequence":"additional","affiliation":[]},{"given":"Abhik","family":"Pal","sequence":"additional","affiliation":[]},{"given":"Benedikt","family":"Stock","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,7,3]]},"reference":[{"key":"2_CR1","unstructured":"Archive of formal proofs. \n                    https:\/\/www.isa-afp.org\/index.html"},{"key":"2_CR2","unstructured":"Write the docs. \n                    https:\/\/www.writethedocs.org\/"},{"key":"2_CR3","unstructured":"Boyer, R., et al.: The QED manifesto. In: Bundy, A. (ed.) Automated Deduction \u2013 CADE 12. LNAI, vol. 814, pp. 238\u2013251. Springer, Heidelberg (1994). \n                    http:\/\/www.cs.ru.nl\/~freek\/qed\/qed.ps.gz"},{"key":"2_CR4","unstructured":"The Coq proof assistant (2019). \n                    http:\/\/coq.inria.fr"},{"issue":"4","key":"2_CR5","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1016\/j.jal.2005.10.001","volume":"4","author":"C Benzm\u00fcller","year":"2006","unstructured":"Benzm\u00fcller, C.: Towards computer aided mathematics. J. Appl. Logic 4(4), 359\u2013365 (2006). \n                    https:\/\/doi.org\/10.1016\/j.jal.2005.10.001","journal-title":"J. Appl. Logic"},{"issue":"1835","key":"2_CR6","doi-asserted-by":"publisher","first-page":"2331","DOI":"10.1098\/rsta.2005.1660","volume":"363","author":"A Bundy","year":"2005","unstructured":"Bundy, A.: Preface. Philos. Trans.: Math. Phys. Eng. Sci. 363(1835), 2331\u20132333 (2005). \n                    http:\/\/www.jstor.org\/stable\/30039730","journal-title":"Philos. Trans.: Math. Phys. Eng. Sci."},{"key":"2_CR7","unstructured":"Buzzard, K.: Xena. \n                    https:\/\/xenaproject.wordpress.com"},{"key":"2_CR8","unstructured":"Django Software Foundation, Contributors: Django documentation. \n                    https:\/\/docs.djangoproject.com\/"},{"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). \n                    https:\/\/doi.org\/10.1007\/978-3-642-39634-2_14"},{"key":"2_CR10","doi-asserted-by":"publisher","unstructured":"Hales, T., et al.: A formal proof of the Kepler conjecture. In: Forum of Mathematics, Pi 5, January 2015. \n                    https:\/\/doi.org\/10.1017\/fmp.2017.1","DOI":"10.1017\/fmp.2017.1"},{"key":"2_CR11","unstructured":"Haslbeck, M.P., Wimmer, S.: Proving for fun. \n                    http:\/\/competition.isabelle.systems"},{"key":"2_CR12","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1090\/S0002-9904-1902-00923-3","volume":"8","author":"D Hilbert","year":"1902","unstructured":"Hilbert, D.: Mathematical problems. Bull. Am. Math. Soc. 8, 437\u2013479 (1902). \n                    https:\/\/doi.org\/10.1090\/S0002-9904-1902-00923-3","journal-title":"Bull. Am. Math. Soc."},{"key":"2_CR13","unstructured":"Matiyasevich, Y.: Alfred Tarski\u2019s great algorithm: decidability of elementary algebra and geometry (talk). \n                    https:\/\/logic.pdmi.ras.ru\/~yumat\/talks\/talks.php?istate=state_show_talk&iid=1364"},{"key":"2_CR14","unstructured":"Matiyasevich, Y.: Finite Dirichlet series with partially prescribed zeroes (talk). \n                    https:\/\/logic.pdmi.ras.ru\/~yumat\/talks\/talks.php?istate=state_show_talk&iid=1364"},{"key":"2_CR15","first-page":"279","volume":"191","author":"Y Matiyasevich","year":"1970","unstructured":"Matiyasevich, Y.: The Diophantineness of enumerable sets. Dokl. Akad. Nauk SSSR 191, 279\u2013282 (1970)","journal-title":"Dokl. Akad. Nauk SSSR"},{"key":"2_CR16","volume-title":"Hilbert\u2019s Tenth Problem","author":"Y Matiyasevich","year":"1993","unstructured":"Matiyasevich, Y.: Hilbert\u2019s Tenth Problem. MIT Press, Cambridge (1993)"},{"key":"2_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics With Isabelle\/HOL","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics With Isabelle\/HOL. Springer, Heidelberg (2014). \n                    https:\/\/doi.org\/10.1007\/978-3-319-10542-0"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). \n                    https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"2_CR19","doi-asserted-by":"publisher","unstructured":"Stock, B., et al.: Hilbert meets Isabelle. In: Isabelle Workshop (Federated Logic Conference) (2018). \n                    https:\/\/doi.org\/10.29007\/3q4s","DOI":"10.29007\/3q4s"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-39634-2_13","volume-title":"Interactive Theorem Proving","author":"J Xu","year":"2013","unstructured":"Xu, J., Zhang, X., Urban, C.: Mechanising turing machines and computability theory in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 147\u2013162. Springer, Heidelberg (2013). \n                    https:\/\/doi.org\/10.1007\/978-3-642-39634-2_13"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-23250-4_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,2]],"date-time":"2019-07-02T03:03:13Z","timestamp":1562036593000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-23250-4_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030232498","9783030232504"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-23250-4_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"3 July 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2019\/cicm.php?event=&menu=general","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}