{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T01:53:18Z","timestamp":1768009998893,"version":"3.49.0"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030535179","type":"print"},{"value":"9783030535186","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-53518-6_22","type":"book-chapter","created":{"date-parts":[[2020,7,17]],"date-time":"2020-07-17T15:17:50Z","timestamp":1594999070000},"page":"303-308","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["Dataset Description: Formalization of Elementary Number Theory in Mizar"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4224-9798","authenticated-orcid":false,"given":"Adam","family":"Naumowicz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,7,17]]},"reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-642-22673-1_19","volume-title":"Intelligent Computer Mathematics","author":"J Alama","year":"2011","unstructured":"Alama, J.: mizar-items: exploring fine-grained dependencies in the Mizar mathematical library. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) CICM 2011. LNCS, vol. 6824, pp. 276\u2013277. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22673-1_19"},{"issue":"1\u20134","key":"22_CR2","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s10817-017-9440-6","volume":"61","author":"G Bancerek","year":"2018","unstructured":"Bancerek, G., et al.: The role of the Mizar mathematical library for interactive proof development in Mizar. J. Autom. Reason. 61(1\u20134), 9\u201332 (2018)","journal-title":"J. Autom. Reason."},{"key":"22_CR3","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"},{"issue":"3\u20134","key":"22_CR4","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. Reasoning 29(3\u20134), 189\u2013224 (2002)","journal-title":"J. Autom. Reasoning"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Grabowski, A.: Tarski\u2019s geometry modelled in Mizar computerized proof assistant. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Proceedings of the 2016 Federated Conference on Computer Science and Information Systems, FedCSIS 2016, Gda\u0144sk, Poland, 11\u201314 September 2016. Annals of Computer Science and Information Systems, vol. 8, pp. 373\u2013381. IEEE (2016)","DOI":"10.15439\/2016F290"},{"issue":"2","key":"22_CR6","first-page":"153","volume":"3","author":"A Grabowski","year":"2010","unstructured":"Grabowski, A., Kornilowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formalized Reason. 3(2), 153\u2013245 (2010)","journal-title":"J. Formalized Reason."},{"issue":"3","key":"22_CR7","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":"22_CR8","first-page":"238","volume":"44","author":"A Kornilowicz","year":"2015","unstructured":"Kornilowicz, A.: Flexary connectives in Mizar. Comput. Lang. Syst. Struct. 44, 238\u2013250 (2015)","journal-title":"Comput. Lang. Syst. Struct."},{"issue":"4","key":"22_CR9","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1515\/forma-2016-0026","volume":"24","author":"A Kornilowicz","year":"2016","unstructured":"Kornilowicz, A., Naumowicz, A.: Niven\u2019s theorem. Formalized Math. 24(4), 301\u2013308 (2016)","journal-title":"Formalized Math."},{"issue":"4","key":"22_CR10","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1016\/j.jal.2005.10.003","volume":"4","author":"A Naumowicz","year":"2006","unstructured":"Naumowicz, A.: An example of formalizing recent mathematical results in Mizar. J. Appl. Log. 4(4), 396\u2013413 (2006)","journal-title":"J. Appl. Log."},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-319-20615-8_26","volume-title":"Intelligent Computer Mathematics","author":"A Naumowicz","year":"2015","unstructured":"Naumowicz, A.: Tools for MML environment analysis. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 348\u2013352. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-20615-8_26"},{"key":"22_CR12","series-title":"Advances in Intelligent Systems and Computing","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-319-67229-8_15","volume-title":"Information Systems Architecture and Technology: Proceedings of 38th International Conference on Information Systems Architecture and Technology \u2013 ISAT 2017","author":"A Naumowicz","year":"2018","unstructured":"Naumowicz, A.: Towards standardized Mizar environments. In: \u015awiatek, J., Borzemski, L., Wilimowska, Z. (eds.) ISAT 2017. AISC, vol. 656, pp. 166\u2013175. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-67229-8_15"},{"issue":"1","key":"22_CR13","doi-asserted-by":"publisher","first-page":"115","DOI":"10.2478\/forma-2020-0010","volume":"28","author":"A Naumowicz","year":"2020","unstructured":"Naumowicz, A.: Elementary number theory problems. Part I. Formalized Math. 28(1), 115\u2013120 (2020)","journal-title":"Part I. Formalized Math."},{"key":"22_CR14","volume-title":"250 Problems in Elementary Number Theory","author":"W Sierpi\u0144ski","year":"1970","unstructured":"Sierpi\u0144ski, W.: 250 Problems in Elementary Number Theory. Elsevier, Amsterdam (1970)"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/11618027_23","volume-title":"Mathematical Knowledge Management","author":"J Urban","year":"2006","unstructured":"Urban, J.: XML-izing Mizar: making semantic processing and presentation of MML easy. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol. 3863, pp. 346\u2013360. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11618027_23"},{"issue":"4","key":"22_CR16","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1016\/j.jal.2005.10.004","volume":"4","author":"J Urban","year":"2006","unstructured":"Urban, J.: Mizarmode - an integrated proof assistance tool for the Mizar way of formalizing mathematics. J. Appl. Log. 4(4), 414\u2013427 (2006)","journal-title":"J. Appl. Log."},{"issue":"2","key":"22_CR17","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10817-012-9269-y","volume":"50","author":"J Urban","year":"2013","unstructured":"Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. J. Autom. Reason. 50(2), 229\u2013241 (2013)","journal-title":"J. Autom. Reason."},{"key":"22_CR18","unstructured":"Wiedijk, F.: Formal proof sketches. https:\/\/www.cs.ru.nl\/~freek\/pubs\/sketches2.pdf"}],"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-030-53518-6_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,24]],"date-time":"2021-04-24T02:14:13Z","timestamp":1619230453000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-53518-6_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030535179","9783030535186"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-53518-6_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 July 2020","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":"Bertinoro","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cicm-conference.org\/2020\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"35","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}