{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T19:33:13Z","timestamp":1725910393506},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319672281"},{"type":"electronic","value":"9783319672298"}],"license":[{"start":{"date-parts":[[2017,9,7]],"date-time":"2017-09-07T00:00:00Z","timestamp":1504742400000},"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":[[2018]]},"DOI":"10.1007\/978-3-319-67229-8_15","type":"book-chapter","created":{"date-parts":[[2017,9,6]],"date-time":"2017-09-06T01:53:54Z","timestamp":1504662834000},"page":"166-175","source":"Crossref","is-referenced-by-count":3,"title":["Towards Standardized Mizar Environments"],"prefix":"10.1007","author":[{"given":"Adam","family":"Naumowicz","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,9,7]]},"reference":[{"key":"15_CR1","unstructured":"Harrison, J.: HOL Light tutorial. http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light\/tutorial.pdf . Accessed 18 May 2017"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development - Coq\u2019Art: the calculus of inductive constructions. In: Texts in Theoretical Computer Science. An EATCS Series. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"15_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, vol. 2283. Springer, New York (2002)"},{"issue":"3","key":"15_CR4","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/s10817-015-9345-1","volume":"55","author":"A Grabowski","year":"2015","unstructured":"Grabowski, A., Korni\u0142owicz, A., Naumowicz, A.: Four decades of Mizar. J. Autom. Reason. 55(3), 191\u2013198 (2015)","journal-title":"J. Autom. Reason."},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Bancerek, G., Byli\u0144ski, C., Grabowski, A., Korni\u0142owicz, A., Matuszewski, R., Naumowicz, A., P\u0105k, K., Urban, J.: Mizar: state-of-the-art and beyond. In: [24], pp. 261\u2013279 (2015)","DOI":"10.1007\/978-3-319-20615-8_17"},{"key":"15_CR6","doi-asserted-by":"crossref","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.) Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011, and Proceedings of 10th International Conference, MKM 2011, Bertinoro, Italy, 18\u201323 July 2011. Lecture Notes in Computer Science, vol. 6824, pp. 276\u2013277. Springer (2011)","DOI":"10.1007\/978-3-642-22673-1_19"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Haslbeck, M., Matichuk, D., Nipkow, T.: Mining the Archive of formal proofs. In: [24], pp. 3\u201317 (2015)","DOI":"10.1007\/978-3-319-20615-8_1"},{"issue":"3","key":"15_CR8","first-page":"385","volume":"2","author":"ST Czuba","year":"1991","unstructured":"Czuba, S.T.: Schemes. Formaliz. Math. 2(3), 385\u2013391 (1991)","journal-title":"Formaliz. Math."},{"issue":"4","key":"15_CR9","first-page":"481","volume":"13","author":"A Korni\u0142owicz","year":"2005","unstructured":"Korni\u0142owicz, A.: Jordan curve theorem. Formaliz. Math. 13(4), 481\u2013491 (2005)","journal-title":"Formaliz. Math."},{"issue":"1","key":"15_CR10","first-page":"67","volume":"1","author":"Z Trybulec","year":"1990","unstructured":"Trybulec, Z.: Properties of subsets. Formaliz. Math. 1(1), 67\u201371 (1990)","journal-title":"Formaliz. Math."},{"issue":"2","key":"15_CR11","first-page":"153","volume":"3","author":"A Grabowski","year":"2010","unstructured":"Grabowski, A., Korni\u0142owicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formaliz. Reason. 3(2), 153\u2013245 (2010)","journal-title":"J. Formaliz. Reason."},{"issue":"31","key":"15_CR12","first-page":"89","volume":"18","author":"A Naumowicz","year":"2009","unstructured":"Naumowicz, A.: Enhanced processing of adjectives in Mizar. Stud. Log. Gramm. Rhetor. 18(31), 89\u2013101 (2009)","journal-title":"Stud. Log. Gramm. Rhetor."},{"issue":"2","key":"15_CR13","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/s10817-012-9261-6","volume":"50","author":"A Korni\u0142owicz","year":"2013","unstructured":"Korni\u0142owicz, A.: On rewriting rules in Mizar. J. Autom. Reason. 50(2), 203\u2013210 (2013)","journal-title":"J. Autom. Reason."},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Grabowski, A., Korni\u0142owicz, A., Schwarzweller, C.: Equality in computer proof-assistants. In: 2015 Federated Conference on Computer Science and Information Systems, FedCSIS 2015, \u0141\u00f3d\u017a, Poland, 13\u201316 September 2015, pp. 45\u201354 (2015)","DOI":"10.15439\/2015F229"},{"issue":"3","key":"15_CR15","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1007\/s10817-015-9331-7","volume":"55","author":"A Korni\u0142owicz","year":"2015","unstructured":"Korni\u0142owicz, A.: Definitional expansions in Mizar. J. Autom. Reason. 55(3), 257\u2013268 (2015)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"15_CR16","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1007\/s10817-015-9332-6","volume":"55","author":"A Naumowicz","year":"2015","unstructured":"Naumowicz, A.: Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver. J. Autom. Reason. 55(3), 285\u2013294 (2015)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"15_CR17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1080\/00207160701864459","volume":"87","author":"A Naumowicz","year":"2010","unstructured":"Naumowicz, A.: Interfacing external CA systems for Gr\u00f6bner bases computation in Mizar proof checking. Int. J. Comput. Math. 87(1), 1\u201311 (2010)","journal-title":"Int. J. Comput. Math."},{"issue":"2","key":"15_CR18","first-page":"161","volume":"3","author":"C Byli\u0144ski","year":"1992","unstructured":"Byli\u0144ski, C.: Cartesian categories. Formaliz. Math. 3(2), 161\u2013169 (1992)","journal-title":"Formaliz. Math."},{"issue":"1","key":"15_CR19","first-page":"17","volume":"1","author":"Z Trybulec","year":"1990","unstructured":"Trybulec, Z., \u015awi\u0119czkowska, H.: Boolean properties of sets. Formaliz. Math. 1(1), 17\u201323 (1990)","journal-title":"Formaliz. Math."},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Naumowicz, A.: Tools for MML environment analysis. In: [24], pp. 348\u2013352 (2015)","DOI":"10.1007\/978-3-319-20615-8_26"},{"issue":"3\u20134","key":"15_CR21","doi-asserted-by":"crossref","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. Reason. 29(3\u20134), 189\u2013224 (2002)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"15_CR22","first-page":"145","volume":"6","author":"A Korni\u0142owicz","year":"1997","unstructured":"Korni\u0142owicz, A.: Cartesian products of relations and relational structures. Formaliz. Math. 6(1), 145\u2013152 (1997)","journal-title":"Formaliz. Math."},{"issue":"1","key":"15_CR23","first-page":"35","volume":"7","author":"G Bancerek","year":"1998","unstructured":"Bancerek, G.: Bases and refinements of topologies. Formaliz. Math. 7(1), 35\u201343 (1998)","journal-title":"Formaliz. Math."},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.): Intelligent Computer Mathematics - International Conference, CICM 2015, Proceedings. Washington, DC, USA, 13\u201317 July 2015. Lecture Notes in Computer Science, vol. 9150. Springer (2015)","DOI":"10.1007\/978-3-319-20615-8"}],"container-title":["Advances in Intelligent Systems and Computing","Information Systems Architecture and Technology: Proceedings of 38th International Conference on Information Systems Architecture and Technology \u2013 ISAT 2017"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67229-8_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,3]],"date-time":"2019-10-03T04:58:49Z","timestamp":1570078729000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-67229-8_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,7]]},"ISBN":["9783319672281","9783319672298"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67229-8_15","relation":{},"ISSN":["2194-5357","2194-5365"],"issn-type":[{"type":"print","value":"2194-5357"},{"type":"electronic","value":"2194-5365"}],"subject":[],"published":{"date-parts":[[2017,9,7]]}}}