{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:49:06Z","timestamp":1725558546825},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642141270"},{"type":"electronic","value":"9783642141287"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14128-7_38","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T06:45:36Z","timestamp":1277793936000},"page":"455-469","source":"Crossref","is-referenced-by-count":19,"title":["A Wiki for Mizar: Motivation, Considerations, and Initial Prototype"],"prefix":"10.1007","author":[{"given":"Josef","family":"Urban","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jesse","family":"Alama","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Piotr","family":"Rudnicki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Herman","family":"Geuvers","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"38_CR1","unstructured":"The Archive of Formal Proofs, \n                    \n                      http:\/\/afp.sourceforge.net\/"},{"key":"38_CR2","unstructured":"Wikiwikiweb, \n                    \n                      http:\/\/c2.com\/cgi\/wiki?WikiWikiWeb"},{"key":"38_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-540-73086-6_19","volume-title":"Towards Mechanized Mathematical Assistants","author":"P. Corbineau","year":"2007","unstructured":"Corbineau, P., Kaliszyk, C.: Cooperative repositories for formal proofs. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM\/CALCULEMUS 2007. LNCS (LNAI), vol.\u00a04573, pp. 221\u2013234. Springer, Heidelberg (2007)"},{"key":"38_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-540-27818-4_7","volume-title":"Mathematical Knowledge Management","author":"L. Cruz-Filipe","year":"2004","unstructured":"Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-CoRN, the Constructive coq Repository at Nijmegen. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol.\u00a03119, pp. 88\u2013103. Springer, Heidelberg (2004)"},{"issue":"7","key":"38_CR5","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","volume":"27","author":"V. D\u2019Silva","year":"2008","unstructured":"D\u2019Silva, V., Kroening, D., Weissenbacher, G.: A Survey of Automated Techniques for Formal Software Verification. IEEE Transactions on Computer-aided Design of Integrated Circuits and Systems\u00a027(7), 1165\u20131178 (2008)","journal-title":"IEEE Transactions on Computer-aided Design of Integrated Circuits and Systems"},{"key":"38_CR6","unstructured":"Git - fast version control system, \n                    \n                      http:\/\/git-scm.com\/"},{"issue":"11","key":"38_CR7","first-page":"1382","volume":"55","author":"G. Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal proof\u2014the four-color theorem. Notices of the American Mathematical Society\u00a055(11), 1382\u20131393 (2008)","journal-title":"Notices of the American Mathematical Society"},{"issue":"3","key":"38_CR8","doi-asserted-by":"publisher","first-page":"1065","DOI":"10.4007\/annals.2005.162.1065","volume":"162","author":"T. Hales","year":"2005","unstructured":"Hales, T.: A proof of the Kepler conjecture. Annals of Mathematics\u00a0162(3), 1065\u20131185 (2005)","journal-title":"Annals of Mathematics"},{"issue":"11","key":"38_CR9","first-page":"1370","volume":"55","author":"T. Hales","year":"2008","unstructured":"Hales, T.: Formal proof. Notices of the American Mathematical Society\u00a055(11), 1370\u20131381 (2008)","journal-title":"Notices of the American Mathematical Society"},{"key":"38_CR10","first-page":"1395","volume":"55","author":"J. Harrison","year":"2008","unstructured":"Harrison, J.: Formal Proof \u2013 Theory and Practice. Notices of the American Mathematical Society\u00a055, 1395\u20131406 (2008)","journal-title":"Notices of the American Mathematical Society"},{"key":"38_CR11","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1145\/1629575.1629596","volume-title":"Proceedings of the 22nd ACM Symposium on Operating Systems Principles","author":"G. Klein","year":"2009","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: Anderson, T. (ed.) Proceedings of the 22nd ACM Symposium on Operating Systems Principles, pp. 207\u2013220. ACM Press, New York (2009)"},{"key":"38_CR12","unstructured":"Mathoverflow, \n                    \n                      http:\/\/mathoverflow.net\/"},{"key":"38_CR13","unstructured":"Wolfram MathWorld: The Web\u2019s Most Extensive Mathematics Resource, \n                    \n                      http:\/\/mathworld.wolfram.com\/"},{"issue":"1","key":"38_CR14","first-page":"3","volume":"4","author":"R. Matuszewski","year":"2005","unstructured":"Matuszewski, R., Rudnicki, P.: MIZAR: the first 30 years. Mechanized Mathematics and its Applications\u00a04(1), 3\u201324 (2005)","journal-title":"Mechanized Mathematics and its Applications"},{"key":"38_CR15","unstructured":"The Mizar Mathematical Library, \n                    \n                      http:\/\/mizar.org\/library\/"},{"key":"38_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/978-3-642-03359-9_5","volume-title":"TPHOLs","author":"A. Naumowicz","year":"2009","unstructured":"Naumowicz, A., Kornilowicz, A.: A Brief Overview of Mizar. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 67\u201372. Springer, Heidelberg (2009)"},{"key":"38_CR17","unstructured":"Planetmath, \n                    \n                      http:\/\/planetmath.org\/"},{"key":"38_CR18","unstructured":"The polymath blog, \n                    \n                      http:\/\/polymathprojects.org\/"},{"key":"38_CR19","unstructured":"Proofwiki, \n                    \n                      http:\/\/www.proofwiki.org\/wiki\/Main_Page"},{"key":"38_CR20","unstructured":"The QED Manifesto. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol.\u00a0814, pp. 238\u2013251. Springer, Heidelberg (1994)"},{"key":"38_CR21","unstructured":"The QPQ Deductive Software Repository, \n                    \n                      http:\/\/www.qpq.org"},{"key":"38_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-36469-2_13","volume-title":"Mathematical Knowledge Management","author":"P. Rudnicki","year":"2003","unstructured":"Rudnicki, P., Trybulec, A.: On the integrity of a repository of formalized mathematics. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol.\u00a02594, pp. 162\u2013174. Springer, Heidelberg (2003)"},{"key":"38_CR23","unstructured":"Trigdell, A.: Efficient Algorithms for Sorting and Synchronization. Ph.D. thesis, Australian National University (1999)"},{"issue":"1-2","key":"38_CR24","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s10817-006-9032-3","volume":"37","author":"J. Urban","year":"2006","unstructured":"Urban, J.: MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning\u00a037(1-2), 21\u201343 (2006)","journal-title":"J. Autom. Reasoning"},{"key":"38_CR25","unstructured":"vdash: What is vdash?, \n                    \n                      http:\/\/www.vdash.org\/intro\/"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14128-7_38.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T08:19:14Z","timestamp":1619770754000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14128-7_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642141270","9783642141287"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14128-7_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}