{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T06:25:23Z","timestamp":1748413523974,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540230298"},{"type":"electronic","value":"9783540278184"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"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":[[2004]]},"DOI":"10.1007\/978-3-540-27818-4_4","type":"book-chapter","created":{"date-parts":[[2010,2,25]],"date-time":"2010-02-25T14:26:47Z","timestamp":1267108007000},"page":"44-57","source":"Crossref","is-referenced-by-count":15,"title":["Integrated Semantic Browsing of the Mizar Mathematical Library for Authoring Mizar Articles"],"prefix":"10.1007","author":[{"given":"Grzegorz","family":"Bancerek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"4_CR1","first-page":"377","volume":"2","author":"G. Bancerek","year":"1990","unstructured":"Bancerek, G.: Cardinal numbers. Formalized Mathematics\u00a02(1), 377\u2013382 (1990), http:\/\/mizar.uwb.edu.pl\/JFM\/Vol1\/card_1.abs.html","journal-title":"Formalized Mathematics"},{"key":"4_CR2","unstructured":"Bancerek, G.: MML Query, description, http:\/\/megrez.mizar.org\/mmlquery\/description.html"},{"key":"4_CR3","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. (eds.) MKM 2003. LNCS, vol.\u00a02594, pp. 119\u2013132. Springer, Heidelberg (2003)"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Borenstein, N.: The text\/enriched MIME Content-type (09\/23\/1993), ftp:\/\/ftp.rfc-editor.org\/in-notes\/rfc1523.txt","DOI":"10.17487\/rfc1523"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Borenstein, N.: The text\/enriched MIME Content-type (01\/10\/ 1994), ftp:\/\/ftp.rfc-editor.org\/in-notes\/rfc1563.txt","DOI":"10.17487\/rfc1563"},{"key":"4_CR6","unstructured":"The grammar of the Mizar library items, http:\/\/merak.pb.bialystok.pl\/mmlquery\/mmlquery.html#Library-item"},{"key":"4_CR7","unstructured":"Journal of Formalized Mathematics, http:\/\/mizar.uwb.edu.pl\/JFM\/"},{"key":"4_CR8","unstructured":"The Mizar Home Page, http:\/\/mizar.org"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Resnick, P., Walker, A.: The text\/enriched MIME Content-type (January 1996), ftp:\/\/ftp.rfc-editor.org\/in-notes\/rfc1896.txt","DOI":"10.17487\/rfc1896"},{"key":"4_CR10","unstructured":"Rudnicki, P.: An overview of the Mizar project. In: Proceedings of the 1992, Workshop on Types for Proofs and Programs. Chalmers University of Technology, Bastad (1992)"},{"key":"4_CR11","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. An experiment in MIZAR. Journal of Automated Reasoning\u00a023, 197\u2013234 (1999)","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR12","unstructured":"Urban, J.: MizarMode: Emacs Authoring Environment for Mizar, available online at: http:\/\/kti.mff.cuni.cz\/~urban\/MizarModeDoc\/html\/"},{"key":"4_CR13","unstructured":"Urban, J.: MoMM \u2013 Fast interreduction and retrieval in large libraries of formalized mathematics. In: Sutcliffe, G., Schultz, S., Tammit, T. (eds.) Proceedings of the IJCAR 2004 Workshop on Empirically Successful First Order Reasoning, ENTCS (accepted, 2004), Available online at: http:\/\/ktiml.mff.cuni.cz\/~urban\/MoMM\/momm.ps"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Urban, J.: MPTP \u2013 Motivation, implementation, first experiments. In: Dahn, I., Kapur, D., Vigneron, L. (eds.) Journal of Automated Reasoning, First-Order Theorem Proving Special Issue. Kluwer Academic Publishers, Dordrecht (supposed publication: end of 2004) (accepted), Available online at: http:\/\/kti.ms.mff.cuni.cz\/~urban\/MPTP\/mptp-jar.ps.gz","DOI":"10.1007\/s10817-004-6245-1"}],"container-title":["Lecture Notes in Computer Science","Mathematical Knowledge Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27818-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T07:50:11Z","timestamp":1558857011000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27818-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540230298","9783540278184"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27818-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}