{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:16:18Z","timestamp":1742912178810,"version":"3.40.3"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661063"},{"type":"electronic","value":"9783319661070"}],"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_32","type":"book-chapter","created":{"date-parts":[[2017,8,20]],"date-time":"2017-08-20T14:13:59Z","timestamp":1503238439000},"page":"514-530","source":"Crossref","is-referenced-by-count":2,"title":["Formalization of the Fundamental Group in Untyped Set Theory Using Auto2"],"prefix":"10.1007","author":[{"given":"Bohua","family":"Zhan","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"32_CR1","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. Formalized Reason. 9(1), 101\u2013148 (2016)","journal-title":"J. Formalized Reason."},{"key":"32_CR2","unstructured":"Bourbaki, N.: Theory of Sets. Springer, Heidelberg (2000)"},{"key":"32_CR3","unstructured":"Brunerie, G.: On the homotopy groups of spheres in homotopy type theory. Ph.D. thesis. https:\/\/arxiv.org\/abs\/1606.05916"},{"key":"32_CR4","unstructured":"Grabowski, A., Kornilowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formaliz. Reason. Spec. Issue: User Tutor. I 3(2), 153\u2013245 (2010)"},{"key":"32_CR5","unstructured":"IsarMathLib. http:\/\/www.nongnu.org\/isarmathlib\/"},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Pak, K., Urban, J.: Towards a Mizar environment for Isabelle: foundations and language. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016), New York, pp. 58\u201365 (2016)","DOI":"10.1145\/2854065.2854070"},{"issue":"3","key":"32_CR7","first-page":"261","volume":"12","author":"A Kornilowicz","year":"2004","unstructured":"Kornilowicz, A., Shidama, Y., Grabowski, A.: The fundamental group. Formalized Math. 12(3), 261\u2013268 (2004)","journal-title":"Formalized Math."},{"key":"32_CR8","unstructured":"Kuncar, O.: Reconstruction of the Mizar type system in the HOL light system. In: Pavlu, J., Safrankova, J. (eds.) WDS Proceedings of Contributed Papers: Part I - Mathematics and Computer Sciences, pp. 7\u201312. Matfyzpress (2010)"},{"key":"32_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-540-73086-6_26","volume-title":"Towards Mechanized Mathematical Assistants","author":"G Lee","year":"2007","unstructured":"Lee, G., Rudnici, P.: Alternative aggregates in Mizar. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Calculemus\/MKM 2007. LNCS (LNAI), vol. 4573, pp. 327\u2013341. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-73086-6_26"},{"key":"32_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-642-39634-2_5","volume-title":"Interactive Theorem Proving","author":"A Mahboubi","year":"2013","unstructured":"Mahboubi, A., Tassi, E.: Canonical structures for the working Coq user. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 19\u201334. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39634-2_5"},{"key":"32_CR11","unstructured":"Megill, N.D.: Metamath: a computer language for pure mathematics. http:\/\/us.metamath.org\/downloads\/metamath.pdf"},{"key":"32_CR12","unstructured":"Munkres, J.R.: Topology. Prentice Hall, Upper Saddle River (2000)"},{"key":"32_CR13","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Set theory for verification: I. From foundations to functions. J. Automated Reason. 11(3), 353\u2013389 (1993)","DOI":"10.1007\/BF00881873"},{"key":"32_CR14","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Set theory for verification: II. Induction and recursion. J. Automated Reason. 15(2), 167\u2013215 (1995)","DOI":"10.1007\/BF00881916"},{"key":"32_CR15","unstructured":"Trybulec, A.: Some features of the Mizar language. In: ESPRIT Workshop (1993)"},{"key":"32_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-540-74591-4_28","volume-title":"Theorem Proving in Higher Order Logics","author":"F Wiedijk","year":"2007","unstructured":"Wiedijk, F.: Mizar\u2019s soft type system. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 383\u2013399. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-74591-4_28"},{"key":"32_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-319-43144-4_27","volume-title":"Interactive Theorem Proving","author":"B Zhan","year":"2016","unstructured":"Zhan, B.: AUTO2, a saturation-based heuristic prover for higher-order logic. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 441\u2013456. Springer, Cham (2016). doi:10.1007\/978-3-319-43144-4_27"}],"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_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,29]],"date-time":"2022-09-29T06:08:43Z","timestamp":1664431723000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-66107-0_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661063","9783319661070"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66107-0_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}