{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:32:59Z","timestamp":1725471179066},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540371045"},{"type":"electronic","value":"9783540371069"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11812289_21","type":"book-chapter","created":{"date-parts":[[2006,9,29]],"date-time":"2006-09-29T08:23:44Z","timestamp":1159518224000},"page":"266-279","source":"Crossref","is-referenced-by-count":15,"title":["Information Retrieval and Rendering with MML Query"],"prefix":"10.1007","author":[{"given":"Grzegorz","family":"Bancerek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","unstructured":"Bancerek, G.: Development of the theory of continuous lattices in mizar. In: Kerber, M., Kohlhase, M. (eds.) Symbolic Computation and Automated Reasoning, pp. 65\u201380. A.K.Peters (2001)"},{"issue":"5","key":"21_CR2","first-page":"963","volume":"1","author":"G. Bancerek","year":"1990","unstructured":"Bancerek, G.: The Reflection Theorem. Formalized Mathematics\u00a01(5), 963\u2013972 (1990)","journal-title":"Formalized Mathematics"},{"issue":"3\u20134","key":"21_CR3","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. Journal of Automated Reasoning\u00a029(3\u20134), 189\u2013224 (2002)","journal-title":"Journal of Automated Reasoning"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/3-540-36469-2_10","volume-title":"Mathematical Knowledge Management","author":"G. Bancerek","year":"2003","unstructured":"Bancerek, G., Rudnicki, P.: Information retrieval in MML. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol.\u00a02594, pp. 119\u2013131. Springer, Heidelberg (2003)"},{"key":"21_CR5","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.\u00a03119, pp. 44\u201357. Springer, Heidelberg (2004)"},{"issue":"1","key":"21_CR6","first-page":"49","volume":"13","author":"P. Braselmann","year":"2005","unstructured":"Braselmann, P., Koepke, P.: G\u00f6del\u2019s Completeness Theorem. Formalized Mathema- tics\u00a013(1), 49\u201353 (2005)","journal-title":"Formalized Mathema- tics"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/978-3-540-45155-6_4","volume-title":"Electronic Information and Communication in Mathematics","author":"I. Dahn","year":"2003","unstructured":"Dahn, I.: Management of Informal Mathematics Knowledge\u2013Lessons Learned from the Trial-Solution Project. In: Bai, F., Wegner, B. (eds.) ICM 2002. LNCS, vol.\u00a02730, pp. 29\u201343. Springer, Heidelberg (2003)"},{"key":"21_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-67678-9","volume-title":"A Compendium of Continuous Lattices","author":"G. Gierz","year":"1980","unstructured":"Gierz, G., Hofmann, K.H., Keimel, K., Lawson, J.D., Mislove, M., Scott, D.S.: A Compendium of Continuous Lattices. Springer, Berlin (1980)"},{"key":"21_CR9","unstructured":"Kohlhase, M. (joint work with Bancerek, G.).: Towards mizar Mathematical Library in OMDoc format. In: Electronic Proceedings of the Workshop Mathematics on the Semantic Web, Eindhoven (2003), \n                    \n                      http:\/\/www.win.tue.nl\/dw\/monet\/proceedings\/kohlhase-mizarinomdoc.ps"},{"issue":"4","key":"21_CR10","first-page":"481","volume":"13","author":"A. Korni\u0142owicz","year":"2005","unstructured":"Korni\u0142owicz, A.: Jordan Curve Theorem. Formalized Mathematics\u00a013(4), 481\u2013491 (2005)","journal-title":"Formalized Mathematics"},{"issue":"1","key":"21_CR11","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"},{"issue":"3","key":"21_CR12","first-page":"461","volume":"9","author":"R. Milewski","year":"2001","unstructured":"Milewski, R.: Fundamental Theorem of Algebra. Formalized Mathematics\u00a09(3), 461\u2013470 (2001)","journal-title":"Formalized Mathematics"},{"issue":"3\u20134","key":"21_CR13","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1023\/A:1006218513245","volume":"23","author":"P. Rudnicki","year":"1999","unstructured":"Rudnicki, P., Trybulec, A.: On equivalents of well-foundedness. Journal of Automated Reasoning\u00a023(3\u20134), 197\u2013234 (1999)","journal-title":"Journal of Automated Reasoning"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Urban, J.: MizarMode - an integrated proof assistance tool for the Mizar way of formalizing mathematics. Journal of Applied Logic (2005), doi:10.1016\/j.jal.2005.10.004","DOI":"10.1016\/j.jal.2005.10.004"},{"issue":"1","key":"21_CR15","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1142\/S0218213006002588","volume":"15","author":"J. Urban","year":"2006","unstructured":"Urban, J.: MoMM - fast interreduction and retrieval in large libraries of formalized mathematics. International Journal on Artificial Intelligence Tools\u00a015(1), 109\u2013130 (2006)","journal-title":"International Journal on Artificial Intelligence Tools"},{"key":"21_CR16","series-title":"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.\u00a03863, pp. 346\u2013360. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Mathematical Knowledge Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11812289_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:27:03Z","timestamp":1619508423000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11812289_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371045","9783540371069"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/11812289_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}