{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T04:02:03Z","timestamp":1748491323139,"version":"3.41.0"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031669965"},{"type":"electronic","value":"9783031669972"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-66997-2_19","type":"book-chapter","created":{"date-parts":[[2024,8,3]],"date-time":"2024-08-03T20:03:12Z","timestamp":1722715392000},"page":"337-344","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Remote Verification System for\u00a0Mizar Integrated with\u00a0Emwiki"],"prefix":"10.1007","author":[{"given":"Toshiki","family":"Kai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuta","family":"Teruya","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1110-4342","authenticated-orcid":false,"given":"Kazuhisa","family":"Nakasho","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,29]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Taniguchi, H., Nakasho, K.: Visual studio code extension and auto-completion for Mizar language. In: 2021 Ninth International Symposium on Computing and Networking (CANDAR), pp.\u00a0182\u2013188. IEEE (2021)","DOI":"10.1109\/CANDAR53791.2021.00033"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-540-27818-4_4","volume-title":"Mathematical Knowledge Management","author":"G Bancerek","year":"2004","unstructured":"Bancerek, G., Urban, J.: Integrated semantic browsing of the Mizar mathematical library for authoring Mizar articles. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 44\u201357. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27818-4_4"},{"issue":"2","key":"19_CR3","first-page":"153","volume":"3","author":"A Grabowski","year":"2010","unstructured":"Grabowski, A., Kornilowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formalized Reasoning 3(2), 153\u2013245 (2010)","journal-title":"J. Formalized Reasoning"},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-319-20615-8_17","volume-title":"Intelligent Computer Mathematics","author":"G Bancerek","year":"2015","unstructured":"Bancerek, G., et al.: Mizar: state-of-the-art and beyond. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 261\u2013279. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-20615-8_17"},{"key":"19_CR5","unstructured":"Arias, E.J.G., Pin, B., Jouvelot, P.: jsCoq: towards hybrid theorem proving interfaces. arXiv preprint arXiv:1701.07125 (2017)"},{"key":"19_CR6","unstructured":"Wenzel, M.: Isabelle\/PIDE after 10 years of development. In: 13th International Workshop on User Interfaces for Theorem Provers (UITP 2018), Oxford, UK (2018)"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-39320-4_22","volume-title":"Intelligent Computer Mathematics","author":"C L\u00fcth","year":"2013","unstructured":"L\u00fcth, C., Ring, M.: A web interface for Isabelle: the next generation. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 326\u2013329. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39320-4_22"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/978-3-319-08970-6_30","volume-title":"Interactive Theorem Proving","author":"M Ring","year":"2014","unstructured":"Ring, M., L\u00fcth, C.: Collaborative interactive theorem proving with clide. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 467\u2013482. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08970-6_30"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Xu, H., Zhao, Y.: Isabelle\/cloud: delivering Isabelle\/HOL as a cloud IDE for theorem proving. In: Proceedings of the 14th Asia-Pacific Symposium on Internetware, pp. 313\u2013322 (2023)","DOI":"10.1145\/3609437.3609460"},{"issue":"3","key":"19_CR10","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s10817-015-9330-8","volume":"55","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: Mizar 40 for Mizar 40. J. Autom. Reason. 55(3), 245\u2013256 (2015)","journal-title":"J. Autom. Reason."},{"key":"19_CR11","unstructured":"Jakub\u016dv, J.,et al.: Mizar 60 for Mizar 50. arXiv preprint arXiv:2303.06686 (2023)"},{"key":"19_CR12","unstructured":"Yamamichi, D., Shigenaka, S., Nakasho, K., Wasaki, K.: A web platform for hosting the Mizar mathematical library (2022)"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-031-16681-5_9","volume-title":"Intelligent Computer Mathematics","author":"H Furushima","year":"2022","unstructured":"Furushima, H., Yamamichi, D., Shigenaka, S., Nakasho, K., Wasaki, K.: An integrated web platform for the Mizar mathematical library. In: Buzzard, K., Kutsia, T. (eds.) CICM 2022. LNCS, vol. 13467, pp. 141\u2013146. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-16681-5_9"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-642-22673-1_10","volume-title":"Intelligent Computer Mathematics","author":"J Alama","year":"2011","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.) CICM 2011. LNCS (LNAI), vol. 6824, pp. 133\u2013148. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22673-1_10"},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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 (LNAI), vol. 7961, pp. 152\u2013167. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39320-4_10"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-20615-8_25","volume-title":"Intelligent Computer Mathematics","author":"K Nakasho","year":"2015","unstructured":"Nakasho, K., Shidama, Y.: Documentation generator focusing on symbols for the HTML-ized Mizar library. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 343\u2013347. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-20615-8_25"},{"key":"19_CR17","unstructured":"Shigenaka, S.: Research on quality measurement of the Mizar mathematical library using dependency graph (2022)"},{"key":"19_CR18","unstructured":"Suzuki, S., Nagasaki, M., Nakasho, K.: Classification and dependency visualization of the articles of the Mizar mathematical library. In: MathUI 2023: 14th Workshop on Mathematical User Interaction, 04\u201308 September 2023, Cambridge, UK (2023)"},{"key":"19_CR19","unstructured":"Miyata, H., Matsumoto, R., Nakasho, K.: VSCode extension for the web and coding assistance for the Mizar language. In: MathUI 2023: 14th Workshop on Mathematical User Interaction, 04\u201308 September 2023, Cambridge, UK (2023)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66997-2_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T06:05:40Z","timestamp":1748412340000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66997-2_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031669965","9783031669972"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66997-2_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"29 July 2024","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":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 August 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 August 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2024\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}