{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:21:11Z","timestamp":1747592471173},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319968117"},{"type":"electronic","value":"9783319968124"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-96812-4_1","type":"book-chapter","created":{"date-parts":[[2018,7,17]],"date-time":"2018-07-17T04:26:41Z","timestamp":1531801601000},"page":"1-6","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["System Description: XSL-Based Translator of Mizar to LaTeX"],"prefix":"10.1007","author":[{"given":"Grzegorz","family":"Bancerek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adam","family":"Naumowicz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"issue":"2","key":"1_CR1","first-page":"19","volume":"5","author":"G Bancerek","year":"2006","unstructured":"Bancerek, G.: Automatic translation in Formalized Mathematics. Mech. Math. Appl. 5(2), 19\u201331 (2006)","journal-title":"Mech. Math. Appl."},{"issue":"2","key":"1_CR2","doi-asserted-by":"publisher","first-page":"177","DOI":"10.2478\/v10037-008-0024-0","volume":"16","author":"G Bancerek","year":"2008","unstructured":"Bancerek, G.: Mizar analysis of algorithms: algorithms over integers. Formaliz. Math. 16(2), 177\u2013194 (2008). \nhttps:\/\/doi.org\/10.2478\/v10037-008-0024-0","journal-title":"Formaliz. Math."},{"issue":"1-4","key":"1_CR3","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s10817-017-9440-6","volume":"61","author":"Grzegorz Bancerek","year":"2017","unstructured":"Bancerek, G., Bylinski, C., Grabowski, A., Kornilowicz, A., Matuszewski, R., Naumowicz, A., Pak, K.: The role of the Mizar Mathematical Library for interactive proof development in Mizar. J. Autom. Reason. 61(1\u20134), 9\u201332 (2018). \nhttps:\/\/doi.org\/10.1007\/s10817-017-9440-6","journal-title":"Journal of Automated Reasoning"},{"key":"1_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). \nhttps:\/\/doi.org\/10.1007\/978-3-319-20615-8_17"},{"key":"1_CR5","unstructured":"Bancerek, G., Carlson, P.: Mizar and the machine translation of mathematics documents. \nhttp:\/\/www.mizar.org\/project\/banc_carl93.ps"},{"key":"1_CR6","unstructured":"Borys, L.: On paracompactness of metrizable spaces. Formaliz. Math. 3(1), 81\u201384 (1992). \nhttp:\/\/fm.mizar.org\/1992-3\/pdf3-1\/pcomps_2.pdf"},{"issue":"3","key":"1_CR7","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10817-015-9345-1","volume":"55","author":"Adam Grabowski","year":"2015","unstructured":"Grabowski, A., Korni\u0142owicz, A., Naumowicz, A.: Four decades of Mizar - foreword. J. Autom. Reason. 55(3), 191\u2013198 (2015). \nhttps:\/\/doi.org\/10.1007\/s10817-015-9345-1","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-540-73086-6_20","volume-title":"Towards Mechanized Mathematical Assistants","author":"A Grabowski","year":"2007","unstructured":"Grabowski, A., Schwarzweller, C.: Revisions as an essential tool to maintain mathematical repositories. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Calculemus\/MKM - 2007. LNCS (LNAI), vol. 4573, pp. 235\u2013249. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-73086-6_20"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-319-42547-4_6","volume-title":"Intelligent Computer Mathematics","author":"A Naumowicz","year":"2016","unstructured":"Naumowicz, A., Piliszek, R.: Accessing the Mizar library with a weakly strict Mizar parser. In: Kohlhase, M., Johansson, M., Miller, B., de Moura, L., Tompa, F. (eds.) CICM 2016. LNCS (LNAI), vol. 9791, pp. 77\u201382. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-42547-4_6"},{"key":"1_CR10","unstructured":"Trybulec, A., Rudnicki, P.: A collection of TeXed Mizar abstracts. \nhttp:\/\/www.mizar.org\/project\/TR-89-18.pdf"},{"key":"1_CR11","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). \nhttps:\/\/doi.org\/10.1007\/11618027_23"},{"issue":"4","key":"1_CR12","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."},{"key":"1_CR13","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, 229\u2013241 (2013). \nhttps:\/\/doi.org\/10.1007\/s10817-012-9269-y","journal-title":"J. Autom. Reason."}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96812-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,7,17]],"date-time":"2018-07-17T04:26:57Z","timestamp":1531801617000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96812-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319968117","9783319968124"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96812-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}