{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,28]],"date-time":"2026-06-28T04:57:37Z","timestamp":1782622657482,"version":"3.54.5"},"publisher-location":"Cham","reference-count":61,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319206141","type":"print"},{"value":"9783319206158","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","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":[[2015]]},"DOI":"10.1007\/978-3-319-20615-8_17","type":"book-chapter","created":{"date-parts":[[2015,6,22]],"date-time":"2015-06-22T15:31:23Z","timestamp":1434987083000},"page":"261-279","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":179,"title":["Mizar: State-of-the-art and Beyond"],"prefix":"10.1007","author":[{"given":"Grzegorz","family":"Bancerek","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Czes\u0142aw","family":"Byli\u0144ski","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Adam","family":"Grabowski","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Artur","family":"Korni\u0142owicz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Roman","family":"Matuszewski","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Adam","family":"Naumowicz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Karol","family":"Pa\u0327k","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,6,23]]},"reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-642-22673-1_19","volume-title":"Intelligent Computer Mathematics","author":"J Alama","year":"2011","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.) MKM\/Calculemus 2011. LNCS, vol. 6824, pp. 276\u2013277. Springer, Heidelberg (2011). http:\/\/dx.doi.org\/10.1007\/978-3-642-22673-1_19"},{"key":"17_CR2","unstructured":"Alama, J.: Escape to Mizar from ATPs. In: Fontaine, P., Schmidt, R.A., Schulz, S. (eds.) Third Workshop on Practical Aspects of Automated Reasoning, PAAR-2012, Manchester, UK, 30 June\u20131 July 2012. EPiC Series, vol. 21, pp. 3\u201311. EasyChair (2012). http:\/\/www.easychair.org\/publications\/?page=1559779348"},{"issue":"2","key":"17_CR3","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10817-012-9264-3","volume":"50","author":"J Alama","year":"2013","unstructured":"Alama, J.: Eliciting implicit assumptions of Mizar proofs by property omission. J. Autom. Reasoning 50(2), 123\u2013133 (2013). http:\/\/dx.doi.org\/\n                                        10.1007\/s10817-012-9264-3","journal-title":"J. Autom. Reasoning"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-642-22673-1_10","volume-title":"Intelligent Computer Mathematics","author":"J Alama","year":"2011","unstructured":"Alama, J., Brink, K., Mamane, L., Urban, J.: Large formal wikis: issues and solutions. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) MKM\/Calculemus 2011. LNCS, vol. 6824, pp. 133\u2013148. Springer, Heidelberg (2011). http:\/\/dx.doi.org\/10.1007\/978-3-642-22673-1"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-22673-1_11","volume-title":"Intelligent Computer Mathematics","author":"J Alama","year":"2011","unstructured":"Alama, J., Kohlhase, M., Mamane, L., Naumowicz, A., Rudnicki, P., Urban, J.: Licensing the Mizar mathematical library. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) MKM 2011\/Calculemus 2011. LNCS, vol. 6824, pp. 149\u2013163. Springer, Heidelberg (2011). http:\/\/dx.doi.org\/10.1007\/978-3-642-22673-1_11"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-31374-5_1","volume-title":"Intelligent Computer Mathematics","author":"J Alama","year":"2012","unstructured":"Alama, J., Mamane, L., Urban, J.: Dependencies in formal mathematics: applications and extraction for Coq and Mizar. In: Campbell, J.A., Jeuring, J., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS, vol. 7362, pp. 1\u201316. Springer, Heidelberg (2012). http:\/\/dx.doi.org\/\n                                        10.1007\/978-3-642-31374-5_1"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Anonymous: the QED manifesto. Bundy, A. (ed.) CADE 1994. LNCS, vol. 814. Springer, Heidelberg (1994)","DOI":"10.1136\/bmj.309.6957.814"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-540-27818-4_27","volume-title":"Mathematical Knowledge Management","author":"A Strotmann","year":"2004","unstructured":"Strotmann, A.: The categorial type of OpenMath objects. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 378\u2013392. Springer, Heidelberg (2004)"},{"issue":"2","key":"17_CR9","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."},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/11812289_21","volume-title":"Mathematical Knowledge Management","author":"G Bancerek","year":"2006","unstructured":"Bancerek, G.: Information retrieval and rendering with MML query. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol. 4108, pp. 266\u2013279. Springer, Heidelberg (2006). http:\/\/dx.doi.org\/10.1007\/11812289_21"},{"issue":"3\u20134","key":"17_CR11","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: formalizing recent mathematics. J. Autom. Reason. 29(3\u20134), 189\u2013224 (2002)","journal-title":"J. Autom. Reason."},{"key":"17_CR12","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. 2594, pp. 119\u2013132. Springer, Heidelberg (2003)"},{"key":"17_CR13","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. 3119, pp. 44\u201357. Springer, Heidelberg (2004)"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-31374-5_30","volume-title":"Intelligent Computer Mathematics","author":"C Bylinski","year":"2012","unstructured":"Bylinski, C., Alama, J.: New developments in parsing Mizar. In: Campbell, J.A., Jeuring, J., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 427\u2013431. Springer, Heidelberg (2012)"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-540-27818-4_5","volume-title":"Mathematical Knowledge Management","author":"P Cairns","year":"2004","unstructured":"Cairns, P.: Informalising formal mathematics: searching the Mizar library with latent semantics. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 58\u201372. Springer, Heidelberg (2004)"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-540-68103-8_5","volume-title":"Types for Proofs and Programs","author":"P Corbineau","year":"2008","unstructured":"Corbineau, P.: A declarative language for the Coq proof assistant. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol. 4941, pp. 69\u201384. Springer, Heidelberg (2008). http:\/\/dx.doi.org\/10.1007\/978-3-540-68103-8_5"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/978-3-642-22673-1_22","volume-title":"Intelligent Computer Mathematics","author":"F Botana","year":"2011","unstructured":"Botana, F.: A symbolic companion for interactive geometric systems. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) MKM 2011 and Calculemus 2011. LNCS, vol. 6824, pp. 285\u2013286. Springer, Heidelberg (2011)"},{"issue":"2","key":"17_CR18","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10817-012-9265-2","volume":"50","author":"Y Futa","year":"2013","unstructured":"Futa, Y., Okazaki, H., Shidama, Y.: Formalization of definitions and theorems related to an elliptic curve over a finite prime field by using Mizar. J. Autom. Reason. 50(2), 161\u2013172 (2013). http:\/\/dx.doi.org\/10.1007\/s10817-012-9265-2","journal-title":"J. Autom. Reason."},{"key":"17_CR19","unstructured":"Gow, J., Cairns, P.: Closing the gap between formal and digital libraries of mathematics. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar and Rhetoric, University of Bia\u0142ystok, vol. 10(23), pp. 249\u2013263 (2007). http:\/\/mizar.org\/trybulec65\/"},{"issue":"4","key":"17_CR20","doi-asserted-by":"crossref","first-page":"371","DOI":"10.3233\/FI-2014-1129","volume":"135","author":"A Grabowski","year":"2014","unstructured":"Grabowski, A.: Efficient rough set theory merging. Fundamenta Informaticae 135(4), 371\u2013385 (2014). http:\/\/dx.doi.org\/10.3233\/FI-2014-1129","journal-title":"Fundamenta Informaticae"},{"issue":"2","key":"17_CR21","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. Spec. Issue: User Tutor. I 3(2), 153\u2013245 (2010)","journal-title":"J. Formaliz. Reason. Spec. Issue: User Tutor. I"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/11618027_4","volume-title":"Mathematical Knowledge Management","author":"A Grabowski","year":"2006","unstructured":"Grabowski, A., Schwarzweller, C.: Translating mathematical vernacular into knowledge repositories. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol. 3863, pp. 49\u201364. Springer, Heidelberg (2006). http:\/\/dx.doi.org\/10.1007\/11618027_4"},{"key":"17_CR23","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.) MKM\/CALCULEMUS 2007. LNCS (LNAI), vol. 4573, pp. 235\u2013249. Springer, Heidelberg (2007). http:\/\/dx.doi.org\/10.1007\/978-3-540-73086-6_20"},{"key":"17_CR24","unstructured":"Grabowski, A., Schwarzweller, C.: Towards automatically categorizing mathematical knowledge. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Proceedings of Federated Conference on Computer Science and Information Systems - FedCSIS 2012, Wroclaw, Poland, 9\u201312 September 2012, pp. 63\u201368 (2012)"},{"key":"17_CR25","series-title":"Lecture Notes in Computer Science","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"1996","unstructured":"Harrison, J.: A Mizar mode for HOL. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125. Springer, Heidelberg (1996). http:\/\/dl.acm.org\/citation.cfm?id=646523.694700"},{"issue":"2","key":"17_CR26","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10817-012-9271-4","volume":"50","author":"M Iancu","year":"2013","unstructured":"Iancu, M., Kohlhase, M., Rabe, F., Urban, J.: The Mizar mathematical library in OMDoc: translation and applications. J. Autom. Reason. 50(2), 191\u2013202 (2013). http:\/\/dx.doi.org\/10.1007\/s10817-012-9271-4","journal-title":"J. Autom. Reason."},{"key":"17_CR27","unstructured":"Ja\u015bkowski, S.: On the Rules of Suppositions in Formal Logic. Studia Logica, Nak\u0142adem Seminarjum Filozoficznego Wydzia\u0142u Matematyczno-Przyrodniczego Uniwersytetu Warszawskiego (1934). http:\/\/books.google.pl\/books?id=6w0vRAAACAAJ"},{"key":"17_CR28","unstructured":"Kaliszyk, C., Urban, J.: MizAR 40 for Mizar 40 (2013). CoRR abs\/1310.2805"},{"key":"17_CR29","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J.: Machine learner for automated reasoning 0.4 and 0.5 (2014). Accepted to PAAR 2014, CoRR abs\/1402.2359"},{"issue":"4","key":"17_CR30","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":"2","key":"17_CR31","doi-asserted-by":"publisher","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). http:\/\/dx.doi.org\/10.1007\/s10817-012-9261-6","journal-title":"J. Autom. Reason."},{"key":"17_CR32","unstructured":"Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. In: Mechanized Mathematicsand Its Applications, Special Issue on 30 Years of Mizar, vol. 4, no. 1, pp. 3\u201324 (2005)"},{"issue":"4","key":"17_CR33","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1016\/j.jal.2005.10.003","volume":"4","author":"A Naumowicz","year":"2006","unstructured":"Naumowicz, A.: An example of formalizing recent mathematical results in Mizar. J. Appl. Logic 4(4), 396\u2013413 (2006). http:\/\/www.sciencedirect.com\/\n                                        science\/article\/pii\/S1570868305000686","journal-title":"J. Appl. Logic"},{"key":"17_CR34","unstructured":"Naumowicz, A.: Enhanced processing of adjectives in Mizar. In: Grabowski, A., Naumowicz, A. (eds.) Computer Reconstruction of the Body of Mathematics. Studies in Logic, Grammar and Rhetoric, University of Bia\u0142ystok, vol. 18, no. 31, pp. 89\u2013101 (2009)"},{"issue":"1","key":"17_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1080\/00207160701864459","volume":"87","author":"A Naumowicz","year":"2010","unstructured":"Naumowicz, A.: Interfacing external CA systems for Grobner bases computation in Mizar proof checking. Int. J. Comput. Math. 87(1), 1\u201311 (2010). http:\/\/dx.doi.org\/10.1080\/00207160701864459","journal-title":"Int. J. Comput. Math."},{"key":"17_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-319-08434-3_37","volume-title":"Intelligent Computer Mathematics","author":"A Naumowicz","year":"2014","unstructured":"Naumowicz, A.: SAT-enhanced Mizar proof checking. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS, vol. 8543, pp. 449\u2013452. Springer, Heidelberg (2014). http:\/\/dx.doi.org\/10.1007\/\n                                        978-3-319-08434-3_37"},{"key":"17_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-540-27818-4_21","volume-title":"Mathematical Knowledge Management","author":"A Naumowicz","year":"2004","unstructured":"Naumowicz, A., Byli\u0144ski, C.: Improving Mizar texts with properties and requirements. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 290\u2013301. Springer, Heidelberg (2004). http:\/\/dx.doi.org\/\n                                        10.1007\/978-3-540-27818-4_21"},{"key":"17_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-642-03359-9_5","volume-title":"Theorem Proving in Higher Order Logics","author":"A Naumowicz","year":"2009","unstructured":"Naumowicz, A., Korni\u0142owicz, A.: A brief overview of Mizar. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 67\u201372. Springer, Heidelberg (2009). http:\/\/dx.doi.org\/10.1007\/978-3-642-03359-9_5"},{"issue":"2","key":"17_CR39","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/s10817-012-9267-0","volume":"50","author":"K Pa\u0327k","year":"2013","unstructured":"Pa\u0327k, K.: Methods of lemma extraction in natural deduction proofs. J. Autom. Reason. 50(2), 217\u2013228 (2013). http:\/\/dx.doi.org\/10.1007\/s10817-012-9267-0","journal-title":"J. Autom. Reason."},{"issue":"3","key":"17_CR40","first-page":"1","volume":"10","author":"K Pa\u0327k","year":"2014","unstructured":"Pa\u0327k, K.: Improving legibility of natural deduction proofs is not trivial. Logic. Methods Comput. Sci. 10(3), 1\u201330 (2014). http:\/\/dx.doi.org\/10.2168\/\n                                        LMCS-10(3:23)2014","journal-title":"Logic. Methods Comput. Sci."},{"key":"17_CR41","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 formal mathematics. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol. 2594, pp. 162\u2013174. Springer, Heidelberg (2003)"},{"key":"17_CR42","unstructured":"Syme, D.: DECLARE: a prototype declarative proof system for higher order logic. Technical report, University of Cambridge (1997)"},{"issue":"2","key":"17_CR43","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/s10817-012-9268-z","volume":"50","author":"A Trybulec","year":"2013","unstructured":"Trybulec, A., Korni\u0142owicz, A., Naumowicz, A., Kuperberg, K.: Formal mathematics for mathematicians. J. Autom. Reason. 50(2), 119\u2013121 (2013). http:\/\/dx.doi.org\/\n                                        10.1007\/s10817-012-9268-z","journal-title":"J. Autom. Reason."},{"issue":"31","key":"17_CR44","first-page":"121","volume":"18","author":"J Urban","year":"2009","unstructured":"Urban, J., Sutcliffe, G., Trac, S., Puzis, Y.: Combining Mizar and TPTP semantic presentation and verification tools. Stud. Logic Gramm. Rhetor. 18(31), 121\u2013136 (2009)","journal-title":"Stud. Logic Gramm. Rhetor."},{"issue":"3\u20134","key":"17_CR45","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/s10817-004-6245-1","volume":"33","author":"J Urban","year":"2004","unstructured":"Urban, J.: MPTP - motivation, implementation, first experiments. J. Autom. Reason. 33(3\u20134), 319\u2013339 (2004)","journal-title":"J. Autom. Reason."},{"key":"17_CR46","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)"},{"issue":"4","key":"17_CR47","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 \u2013 an integrated proof assistance tool for the Mizar way of formalizing mathematics. J. Appl. Logic 4(4), 414\u2013427 (2006). http:\/\/dx.doi.org\/\n                                        10.1016\/j.jal.2005.10.004","journal-title":"J. Appl. Logic"},{"issue":"1","key":"17_CR48","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1142\/S0218213006002588","volume":"15","author":"J Urban","year":"2006","unstructured":"Urban, J.: MoMM \u2013 fast interreduction and retrieval in large libraries of formalized mathematics. Int. J. Artif. Intell. Tools 15(1), 109\u2013130 (2006). http:\/\/ktiml.mff.cuni.cz\/urban\/MoMM\/momm.ps","journal-title":"Int. J. Artif. Intell. Tools"},{"issue":"1\u20132","key":"17_CR49","first-page":"21","volume":"37","author":"J Urban","year":"2006","unstructured":"Urban, J.: MPTP 0.2: design, implementation, and initial experiments. J. Autom. Reason. 37(1\u20132), 21\u201343 (2006). http:\/\/dx.doi.org\/10.1007\/s10817-006-9032-3","journal-title":"J. Autom. Reason."},{"key":"17_CR50","unstructured":"Urban, J.: BliStr: The Blind Strategymaker (2014). Accepted to PAAR 2014, CoRR abs\/1301.2683"},{"key":"17_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/978-3-642-14128-7_38","volume-title":"Intelligent Computer Mathematics","author":"J Urban","year":"2010","unstructured":"Urban, J., Alama, J., Rudnicki, P., Geuvers, H.: A wiki for Mizar: motivation, considerations, and initial prototype. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC 2010. LNCS, vol. 6167, pp. 455\u2013469. Springer, Heidelberg (2010)"},{"issue":"2","key":"17_CR52","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(2), 229\u2013241 (2013). http:\/\/dx.doi.org\/10.1007\/\n                                        s10817-012-9269-y","journal-title":"J. Autom. Reason."},{"issue":"2","key":"17_CR53","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/s11786-008-0053-7","volume":"2","author":"J Urban","year":"2008","unstructured":"Urban, J., Sutcliffe, G.: ATP-based cross-verification of Mizar proofs: method, systems, and first experiments. Math. Comput. Sci. 2(2), 231\u2013251 (2008). http:\/\/dx.doi.org\/10.1007\/s11786-008-0053-7","journal-title":"Math. Comput. Sci."},{"key":"17_CR54","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-540-71070-7_37","volume-title":"Automated Reasoning","author":"J Urban","year":"2008","unstructured":"Urban, J., Sutcliffe, G., Pudl\u00e1k, P., Vysko\u010dil, J.: MaLARea SG1 - machine learner for automated reasoning with semantic guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 441\u2013456. Springer, Heidelberg (2008)"},{"key":"17_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-22119-4_21","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"J Urban","year":"2011","unstructured":"Urban, J., Vysko\u010dil, J., \u0160t\u011bp\u00e1nek, P.: MaLeCoP machine learning connection prover. In: Br\u00fcnnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS, vol. 6793, pp. 263\u2013277. Springer, Heidelberg (2011)"},{"issue":"3\u20134","key":"17_CR56","first-page":"389","volume":"29","author":"M Wenzel","year":"2003","unstructured":"Wenzel, M., Wiedijk, F.: A comparison of Mizar and Isar. J. Autom. Reason. 29(3\u20134), 389\u2013411 (2003). http:\/\/dx.doi.org\/10.1023\/A:1021935419355","journal-title":"J. Autom. Reason."},{"key":"17_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/3-540-44755-5_26","volume-title":"Theorem Proving in Higher Order Logics","author":"F Wiedijk","year":"2001","unstructured":"Wiedijk, F.: Mizar light for HOL light. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 378\u2013394. Springer, Heidelberg (2001)"},{"key":"17_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-540-24849-1_24","volume-title":"Types for Proofs and Programs","author":"F Wiedijk","year":"2004","unstructured":"Wiedijk, F.: Formal proof sketches. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 378\u2013393. Springer, Heidelberg (2004)"},{"key":"17_CR59","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/11542384_10","volume-title":"The Seventeen Provers of the World","author":"R Gamboa","year":"2006","unstructured":"Gamboa, R.: ACL2. In: Wiedijk, F. (ed.) The Seventeen Provers of the World. LNCS (LNAI), vol. 3600, pp. 55\u201366. Springer, Heidelberg (2006)"},{"issue":"11","key":"17_CR60","first-page":"1408","volume":"55","author":"F Wiedijk","year":"2008","unstructured":"Wiedijk, F.: Formal proof\u2013getting started. Not. Am. Math. Soc. 55(11), 1408\u20131414 (2008)","journal-title":"Not. Am. Math. Soc."},{"issue":"1:30","key":"17_CR61","first-page":"1","volume":"8","author":"F Wiedijk","year":"2012","unstructured":"Wiedijk, F.: A synthesis of the procedural and declarative styles of interactive theorem proving. Logic. Methods Comput. Sci. 8(1:30), 1\u201326 (2012)","journal-title":"Logic. Methods Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-20615-8_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T02:05:41Z","timestamp":1676945141000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-20615-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319206141","9783319206158"],"references-count":61,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-20615-8_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"23 June 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}