{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T02:38:38Z","timestamp":1768012718790,"version":"3.49.0"},"reference-count":92,"publisher":"Springer Science and Business Media LLC","issue":"1-4","license":[{"start":{"date-parts":[[2017,11,25]],"date-time":"2017-11-25T00:00:00Z","timestamp":1511568000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2018,6]]},"DOI":"10.1007\/s10817-017-9440-6","type":"journal-article","created":{"date-parts":[[2017,11,25]],"date-time":"2017-11-25T10:53:13Z","timestamp":1511607193000},"page":"9-32","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":182,"title":["The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar"],"prefix":"10.1007","volume":"61","author":[{"given":"Grzegorz","family":"Bancerek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Czes\u0142aw","family":"Byli\u0144ski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adam","family":"Grabowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Artur","family":"Korni\u0142owicz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roman","family":"Matuszewski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adam","family":"Naumowicz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karol","family":"P\u0105k","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,11,25]]},"reference":[{"key":"9440_CR1","unstructured":"Abad, P., Abad, J.: The hundred greatest theorems (1999). http:\/\/www.cs.ru.nl\/~freek\/100\/"},{"key":"9440_CR2","doi-asserted-by":"crossref","unstructured":"Adams, A.A., Davenport, J.H.: Copyright issues for MKM. In: Asperti et\u00a0al. [7], pp. 1\u201316. https:\/\/doi.org\/10.1007\/978-3-540-27818-4_1","DOI":"10.1007\/978-3-540-27818-4_1"},{"key":"9440_CR3","doi-asserted-by":"publisher","unstructured":"Alama, J., Brink, K., Mamane, L., Urban, J.: Large formal wikis: issues and solutions. In: Davenport et\u00a0al. [19], pp. 133\u2013148. https:\/\/doi.org\/10.1007\/978-3-642-22673-1_10","DOI":"10.1007\/978-3-642-22673-1_10"},{"key":"9440_CR4","doi-asserted-by":"publisher","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., \u00a0Urban, J., \u00a0Rabe, F. (eds.) Proceedings of the 18th Calculemus and 10th International Conference on Intelligent Computer Mathematics. MKM\u201911, Lecture Notes in Computer Science, vol. 6824, pp. 149\u2013163. Springer, Berlin, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22673-1_11","DOI":"10.1007\/978-3-642-22673-1_11"},{"key":"9440_CR5","doi-asserted-by":"publisher","unstructured":"Alama, J., Mamane, L., Urban, J.: Dependencies in formal mathematics: applications and extraction for Coq and Mizar. In: \u00a0Jeuring, J., Campbell, J.A., \u00a0Carette, J., Reis, G.D., \u00a0Sojka, P., \u00a0Wenzel, M., \u00a0Sorge, V. (eds.) Intelligent Computer Mathematics\u201411th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8\u201313, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7362, pp. 1\u201316. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31374-5_1","DOI":"10.1007\/978-3-642-31374-5_1"},{"key":"9440_CR6","doi-asserted-by":"publisher","unstructured":"Alama, J.: Mizar-items: exploring fine-grained dependencies in the Mizar mathematical library. In: Davenport et\u00a0al. [19], pp. 276\u2013277. https:\/\/doi.org\/10.1007\/978-3-642-22673-1_19","DOI":"10.1007\/978-3-642-22673-1_19"},{"key":"9440_CR7","doi-asserted-by":"crossref","unstructured":"Asperti, A., Bancerek, G., Trybulec, A. (eds.): Mathematical Knowledge Management. In: Proceedings of Third International Conference, MKM 2004, Bialowieza, Poland, September 19\u201321, 2004, Lecture Notes in Computer Science, vol. 3119. Springer (2004)","DOI":"10.1007\/b100478"},{"key":"9440_CR8","doi-asserted-by":"publisher","unstructured":"Aspinall, D., Kaliszyk, C.: Towards formal proof metrics. In: \u00a0Stevens, P., \u00a0Wasowski, A. (eds.) 19th International Conference on Fundamental Approaches to Software Engineering (FASE 2016). Lecture Notes in Computer Science, vol. 9633, pp. 325\u2013341. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49665-7_19","DOI":"10.1007\/978-3-662-49665-7_19"},{"key":"9440_CR9","doi-asserted-by":"publisher","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: Kerber et\u00a0al. [46], pp. 261\u2013279. https:\/\/doi.org\/10.1007\/978-3-319-20615-8_17","DOI":"10.1007\/978-3-319-20615-8_17"},{"key":"9440_CR10","unstructured":"Bancerek, G., Hryniewiecki, K.: Segments of natural numbers and finite sequences. Formalized Math 1(1), 107\u2013114 (1990). http:\/\/fm.mizar.org\/1990-1\/pdf1-1\/finseq_1.pdf"},{"key":"9440_CR11","doi-asserted-by":"publisher","unstructured":"Bancerek, G.: Information retrieval and rendering with MML Query. In: J.\u00a0Borwein, W.\u00a0Farmer (eds.) Mathematical Knowledge Management. Lecture Notes in Computer Science, vol. 4108, pp. 266\u2013279. Springer, Berlin Heidelberg (2006). https:\/\/doi.org\/10.1007\/11812289_21","DOI":"10.1007\/11812289_21"},{"issue":"2","key":"9440_CR12","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":"3\u20134","key":"9440_CR13","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: formalizing recent mathematics. J. Autom. Reason. 29(3\u20134), 189\u2013224 (2002)","journal-title":"J. Autom. Reason."},{"key":"9440_CR14","doi-asserted-by":"publisher","unstructured":"Blanchette, J.C., Haslbeck, M., Matichuk, D., Nipkow, T.: Mining the archive of formal proofs. In: Kerber et\u00a0al. [46], pp. 3\u201317. https:\/\/doi.org\/10.1007\/978-3-319-20615-8_1","DOI":"10.1007\/978-3-319-20615-8_1"},{"issue":"1","key":"9440_CR15","doi-asserted-by":"publisher","first-page":"101","DOI":"10.6092\/issn.1972-5787\/4593","volume":"9","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formaliz. Reason. 9(1), 101\u2013148 (2016). https:\/\/doi.org\/10.6092\/issn.1972-5787\/4593","journal-title":"J. Formaliz. Reason."},{"key":"9440_CR16","doi-asserted-by":"publisher","unstructured":"Borak, E., Zalewska, A.: Mizar Course in Logic and Set Theory, pp. 191\u2013204. Springer Berlin Heidelberg, Berlin, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73086-6_17","DOI":"10.1007\/978-3-540-73086-6_17"},{"key":"9440_CR17","first-page":"235","volume":"18","author":"K Borsuk","year":"1970","unstructured":"Borsuk, K.: On the homotopy types of some decomposition spaces. Bull. Acad. Polon. Sci. 18, 235\u2013239 (1970)","journal-title":"Bull. Acad. Polon. Sci."},{"key":"9440_CR18","unstructured":"Butler, R.W., Sjogren, J.A.: A PVS graph theory library. Technical Report (1998)"},{"key":"9440_CR19","doi-asserted-by":"publisher","unstructured":"Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.): Intelligent Computer Mathematics: 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18\u201323, 2011. Proceedings, Lecture Notes in Computer Science, vol. 6824. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22673-1","DOI":"10.1007\/978-3-642-22673-1"},{"key":"9440_CR20","doi-asserted-by":"crossref","unstructured":"de\u00a0Bruijn, N.: The mathematical language AUTOMATH, its usage, and some of its extensions. In: Laudet, M. (ed.) Proceedings of the Symposium on Automatic Demonstration, pp. 29\u201361. Springer LNM 125, Versailles, France (1968)","DOI":"10.1007\/BFb0060623"},{"key":"9440_CR21","unstructured":"Gauthier, T., Kaliszyk, C., Urban, J.: Initial experiments with statistical conjecturing over large formal corpora. In: Kohlhase, A., Libbrecht P., Miller, B.R.,\u00a0Naumowicz, A., Neuper, W., \u00a0Quaresma, P., Tompa, F.W., Suda, M. (eds.) Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 co-located with the 9th Conference on Intelligent Computer Mathematics (CICM 2016), Bialystok, Poland, July 25\u201329, 2016. CEUR Workshop Proceedings, vol. 1785, pp. 219\u2013228. CEUR-WS.org (2016). http:\/\/ceur-ws.org\/Vol-1785\/W23.pdf"},{"key":"9440_CR22","unstructured":"Gauthier, T., Kaliszyk, C.: Aligning concepts across proof assistant libraries. J. Symbol. Comput. (to appear) (2017)"},{"key":"9440_CR23","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., Keimel, K., Lawson, J., Mislove, M., Scott, D.: A Compendium of Continuous Lattices. Springer, Berlin, Heidelberg, New York (1980)"},{"key":"9440_CR24","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511542725","volume-title":"Continuous Lattices and Domains, Encyclopedia of Mathematics and its Applications","author":"G Gierz","year":"2003","unstructured":"Gierz, G., Hofmann, K., Keimel, K., Lawson, J., Mislove, M., Scott, D.: Continuous Lattices and Domains, Encyclopedia of Mathematics and its Applications, vol. 93. Cambridge University Press, Cambridge (2003)"},{"key":"9440_CR25","doi-asserted-by":"crossref","unstructured":"Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Roux, S.L., Mahboubi, A., O\u2019Connor, R., Biha, S.O., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Th\u00e9ry, L.: A machine-checked proof of the Odd Order Theorem. In: \u00a0Blazy, S.,\u00a0Paulin-Mohring, C.,\u00a0Pichardie, D. (eds.) ITP. Lecture Notes in Computer Science, vol. 7998, pp. 163\u2013179. Springer (2013)","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"9440_CR26","doi-asserted-by":"publisher","unstructured":"Grabowski, A., Korni\u0142owicz, A., Schwarzweller, C.: Equality in computer proof-assistants. In: \u00a0Ganzha, M., Maciaszek, L.A., \u00a0Paprzycki, M. (eds.) Proceedings of the 2015 Federated Conference on Computer Science and Information Systems. Annals of Computer Science and Information Systems, vol.\u00a05, pp. 45\u201354. IEEE (2015). https:\/\/doi.org\/10.15439\/2015F229","DOI":"10.15439\/2015F229"},{"key":"9440_CR27","doi-asserted-by":"publisher","unstructured":"Grabowski, A., Korni\u0142owicz, A., Schwarzweller, C.: On algebraic hierarchies in mathematical repository of Mizar. In: \u00a0Ganzha, M., Maciaszek, L.A., \u00a0Paprzycki, M. (eds.) Proceedings of the 2016 Federated Conference on Computer Science and Information Systems. Annals of Computer Science and Information Systems, vol.\u00a08, pp. 363\u2013371. IEEE (2016). https:\/\/doi.org\/10.15439\/2016F520","DOI":"10.15439\/2016F520"},{"key":"9440_CR28","doi-asserted-by":"publisher","unstructured":"Grabowski, A., Moschner, M.: Managing heterogeneous theories within a\u00a0mathematical knowledge repository. In: Asperti et\u00a0al. [7], pp. 116\u2013129. https:\/\/doi.org\/10.1007\/978-3-540-27818-4_9","DOI":"10.1007\/978-3-540-27818-4_9"},{"key":"9440_CR29","doi-asserted-by":"publisher","unstructured":"Grabowski, A., Schwarzweller, C.: On duplication in mathematical repositories. In: \u00a0Autexier, S., \u00a0Calmet, J., \u00a0Delahaye, D., Ion, P.D.F., \u00a0Rideau, L., \u00a0Rioboo, R., Sexton, A.P. (eds.) Intelligent Computer Mathematics, 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010, Paris, France, July 5\u201310, 2010. Proceedings, Lecture Notes in Computer Science, vol. 6167, pp. 300\u2013314. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-14128-7_26","DOI":"10.1007\/978-3-642-14128-7_26"},{"key":"9440_CR30","doi-asserted-by":"publisher","unstructured":"Grabowski, A., Schwarzweller, C.: Revisions as an essential tool to maintain mathematical repositories. In: Proceedings of the 14th Symposium on Towards Mechanized Mathematical Assistants: 6th International Conference. Calculemus \u201907 \/ MKM \u201907, pp. 235\u2013249. Springer-Verlag, Berlin, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73086-6_20","DOI":"10.1007\/978-3-540-73086-6_20"},{"key":"9440_CR31","doi-asserted-by":"publisher","unstructured":"Grabowski, A.: Expressing the notion of a mathematical structure in the formal language of Mizar. In: \u00a0Gruca, A., \u00a0Czachorski, T., \u00a0Harezlak, K., \u00a0Kozielski, S., \u00a0Piotrowska, A. (eds.) Man-Machine Interactions 5. ICMMI 2017, vol. 659, pp. 261\u2013270. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-67792-7_26","DOI":"10.1007\/978-3-319-67792-7_26"},{"issue":"3","key":"9440_CR32","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/s10817-015-9333-5","volume":"55","author":"A Grabowski","year":"2015","unstructured":"Grabowski, A.: Mechanizing complemented lattices within Mizar type system. J. Autom. Reason. 55(3), 211\u2013221 (2015). https:\/\/doi.org\/10.1007\/s10817-015-9333-5","journal-title":"J. Autom. Reason."},{"issue":"2\u20133","key":"9440_CR33","doi-asserted-by":"publisher","first-page":"223","DOI":"10.3233\/FI-2016-1406","volume":"147","author":"A Grabowski","year":"2016","unstructured":"Grabowski, A.: Lattice theory for rough sets\u2014a case study with Mizar. Fundam. Inform. 147(2\u20133), 223\u2013240 (2016). https:\/\/doi.org\/10.3233\/FI-2016-1406","journal-title":"Fundam. Inform."},{"issue":"2","key":"9440_CR34","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."},{"key":"9440_CR35","doi-asserted-by":"publisher","unstructured":"Grabowski, A., Korni\u0142owicz, A., Naumowicz, A.: Four decades of Mizar. J. Autom. Reason. 55(3), 191\u2013198 (2015). https:\/\/doi.org\/10.1007\/s10817-015-9345-1","DOI":"10.1007\/s10817-015-9345-1"},{"key":"9440_CR36","doi-asserted-by":"publisher","unstructured":"Hales, T., Adams, M., Bauer, G., Dang, T.D., Harrison, J., Hoang, L.T., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T., et\u00a0al.: A\u00a0formal proof of the Kepler conjecture. Forum of Mathematics, Pi 5 (2017). https:\/\/doi.org\/10.1017\/fmp.2017.1","DOI":"10.1017\/fmp.2017.1"},{"issue":"2","key":"9440_CR37","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). https:\/\/doi.org\/10.1007\/s10817-012-9271-4","journal-title":"J. Autom. Reason."},{"key":"9440_CR38","unstructured":"Irving, G., Szegedy, C., Alemi, A.A., E\u00e9n, N., Chollet, F., Urban, J.: Deepmath\u2014deep sequence models for premise selection. In: Lee, D.D., \u00a0Sugiyama, M., \u00a0von Luxburg, U., \u00a0Guyon, I., \u00a0Garnett, R. (eds.) Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016, December 5\u201310, 2016, Barcelona, Spain, pp. 2235\u20132243 (2016). http:\/\/papers.nips.cc\/paper\/6280-deepmath-deep-sequence-models-for-premise-selection"},{"key":"9440_CR39","doi-asserted-by":"publisher","unstructured":"Kaliszyk, C., P\u0105k, K., Urban, J.: Towards a\u00a0Mizar environment for Isabelle: foundations and language. In: \u00a0Avigad, J., \u00a0Chlipala, A. (eds.) Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20\u201322, 2016, pp. 58\u201365. ACM (2016). https:\/\/doi.org\/10.1145\/2854065.2854070","DOI":"10.1145\/2854065.2854070"},{"key":"9440_CR40","doi-asserted-by":"publisher","unstructured":"Kaliszyk, C., Schulz, S., Urban, J., Vysko\u010dil, J.: System description: E.T. 0.1. In: Felty, A.P., \u00a0Middeldorp, A. (eds.) Proceedings of 25th International Conference on Automated Deduction (CADE\u201915). LNCS, vol. 9195, pp. 389\u2013398. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_27","DOI":"10.1007\/978-3-319-21401-6_27"},{"key":"9440_CR41","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J.: Efficient semantic features for automated reasoning over large theories. In: \u00a0Yang, Q., \u00a0Wooldridge, M. (eds.) Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI\u201915), pp. 3084\u20133090. AAAI Press (2015)"},{"key":"9440_CR42","doi-asserted-by":"publisher","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J.: Lemmatization for stronger reasoning in large theories. In: \u00a0Lutz, C., \u00a0Ranise, S. (eds.) Frontiers of Combining Systems (FroCoS\u201915). LNCS, vol. 9322, pp. 341\u2013356. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-24246-0_21","DOI":"10.1007\/978-3-319-24246-0_21"},{"key":"9440_CR43","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J.: System description: Statistical parsing of informalized Mizar formulas (to appear) (2017)","DOI":"10.1109\/SYNASC.2017.00036"},{"key":"9440_CR44","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/j.jsc.2014.09.032","volume":"69","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted theorem proving with millions of lemmas. J. Symbol. Comput. 69, 109\u2013128 (2015). https:\/\/doi.org\/10.1016\/j.jsc.2014.09.032","journal-title":"J. Symbol. Comput."},{"issue":"3","key":"9440_CR45","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s10817-015-9330-8","volume":"55","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: MizAR 40 for Mizar 40. J. Autom. Reason. 55(3), 245\u2013256 (2015). https:\/\/doi.org\/10.1007\/s10817-015-9330-8","journal-title":"J. Autom. Reason."},{"key":"9440_CR46","doi-asserted-by":"publisher","unstructured":"Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.): Intelligent Computer Mathematics\u2014International Conference, CICM 2015, Washington, DC, USA, July 13\u201317, 2015, Proceedings, Lecture Notes in Computer Science, vol. 9150. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-20615-8","DOI":"10.1007\/978-3-319-20615-8"},{"key":"9440_CR47","doi-asserted-by":"publisher","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22-nd Symposium on Operating Systems Principles, SOSP\u201909, pp. 207\u2013220. ACM, New York, NY, USA (2009). https:\/\/doi.org\/10.1145\/1629575.1629596","DOI":"10.1145\/1629575.1629596"},{"key":"9440_CR48","doi-asserted-by":"publisher","unstructured":"Kohlhase, M., Johansson, M., Miller, B.R., de\u00a0Moura, L., Tompa, F.W. (eds.): Intelligent Computer Mathematics. In: Proceedings of the 9th International Conference, CICM 2016, Bialystok, Poland, July 25\u201329, 2016, Lecture Notes in Computer Science, vol. 9791. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-42547-4","DOI":"10.1007\/978-3-319-42547-4"},{"key":"9440_CR49","doi-asserted-by":"publisher","unstructured":"Korni\u0142owicz, A.: Enhancement of Mizar texts with transitivity property of predicates. In: Kohlhase et\u00a0al. [48], pp. 157\u2013162. https:\/\/doi.org\/10.1007\/978-3-319-42547-4_12","DOI":"10.1007\/978-3-319-42547-4_12"},{"issue":"1","key":"9440_CR50","first-page":"33","volume":"6","author":"A Korni\u0142owicz","year":"2007","unstructured":"Korni\u0142owicz, A.: A proof of the Jordan curve theorem via the Brouwer fixed point theorem. Mech. Math. Appl. Spe. Issue Jordan Curve Theorem 6(1), 33\u201340 (2007)","journal-title":"Mech. Math. Appl. Spe. Issue Jordan Curve Theorem"},{"issue":"2","key":"9440_CR51","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). https:\/\/doi.org\/10.1007\/s10817-012-9261-6","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9440_CR52","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/s10817-015-9331-7","journal-title":"J. Autom. Reason."},{"key":"9440_CR53","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1016\/j.cl.2015.07.002","volume":"44","author":"A Korni\u0142owicz","year":"2015","unstructured":"Korni\u0142owicz, A.: Flexary connectives in Mizar. Comput. Lang. Syst. Struct. 44, 238\u2013250 (2015). https:\/\/doi.org\/10.1016\/j.cl.2015.07.002","journal-title":"Comput. Lang. Syst. Struct."},{"issue":"4","key":"9440_CR54","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/s10559-013-9534-z","volume":"49","author":"AA Letichevsky","year":"2013","unstructured":"Letichevsky, A.A., Lyaletski, A.V., Morokhovets, M.K.: Glushkov\u2019s evidence algorithm. Cybern. Syst. Anal. 49(4), 489\u2013500 (2013). https:\/\/doi.org\/10.1007\/s10559-013-9534-z","journal-title":"Cybern. Syst. Anal."},{"key":"9440_CR55","doi-asserted-by":"crossref","unstructured":"Loos, S., Irving, G., Szegedy, C., Kaliszyk, C.: Deep network guided proof search. In: \u00a0Eiter, T., \u00a0Sands, D. (eds.) LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol.\u00a046, pp. 85\u2013105. EasyChair (2017)","DOI":"10.29007\/8mwc"},{"issue":"1","key":"9440_CR56","first-page":"3","volume":"4","author":"R Matuszewski","year":"2005","unstructured":"Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. Mech. Math. Appl. Special Issue on 30 Years of Mizar 4(1), 3\u201324 (2005)","journal-title":"Mech. Math. Appl. Special Issue on 30 Years of Mizar"},{"key":"9440_CR57","unstructured":"Milewski, R.: Fundamental theorem of algebra. Formaliz. Math. 9(3), 461\u2013470 (2001). http:\/\/fm.mizar.org\/2001-9\/pdf9-3\/polynom5.pdf"},{"issue":"1","key":"9440_CR58","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/942578.807067","volume":"7","author":"R Milner","year":"1972","unstructured":"Milner, R.: Implementation and applications of Scott\u2019s logic for computable functions. SIGPLAN Not. 7(1), 1\u20136 (1972). https:\/\/doi.org\/10.1145\/942578.807067","journal-title":"SIGPLAN Not."},{"key":"9440_CR59","doi-asserted-by":"publisher","unstructured":"Naumowicz, A., Byli\u0144ski, C.: Improving Mizar texts with properties and requirements. In: \u00a0Asperti, A.,\u00a0Bancerek, G., \u00a0Trybulec, A. (eds.) Mathematical Knowledge Management, Third International Conference, MKM 2004 Proceedings. MKM\u201904, Lecture Notes in Computer Science, vol. 3119, pp. 290\u2013301 (2004). https:\/\/doi.org\/10.1007\/978-3-540-27818-4_21","DOI":"10.1007\/978-3-540-27818-4_21"},{"key":"9440_CR60","doi-asserted-by":"publisher","unstructured":"Naumowicz, A., Korni\u0142owicz, A.: Introducing Euclidean relations to Mizar. In: \u00a0Ganzha, M., Maciaszek, L.A., \u00a0Paprzycki,M. (eds.) Proceedings of the 2017 Federated Conference on Computer Science and Information Systems, FedCSIS 2017, Prague, Czech Republic, September 3\u20136, 2017. Annals of Computer Science and Information Systems, vol.\u00a011, pp. 245\u2013248. IEEE (2017). https:\/\/doi.org\/10.15439\/2017F368","DOI":"10.15439\/2017F368"},{"key":"9440_CR61","doi-asserted-by":"publisher","unstructured":"Naumowicz, A., Piliszek, R.: Accessing the Mizar library with a\u00a0weakly strict Mizar parser. In: Kohlhase et\u00a0al. [48], pp. 77\u201382. https:\/\/doi.org\/10.1007\/978-3-319-42547-4_6","DOI":"10.1007\/978-3-319-42547-4_6"},{"key":"9440_CR62","unstructured":"Naumowicz, A.: Enhanced processing of adjectives in Mizar. In: \u00a0Grabowski, A.,\u00a0Naumowicz, A. (eds.) Computer Reconstruction of the Body of Mathematics. Studies in Logic, Grammar and Rhetoric, vol. 18(31), pp. 89\u2013101. University of Bia\u0142ystok (2009)"},{"key":"9440_CR63","unstructured":"Naumowicz, A.: Evaluating prospective built-in elements of computer algebra in Mizar. In: \u00a0Matuszewski, R., \u00a0Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar and Rhetoric, vol. 10(23), pp. 191\u2013200. University of Bia\u0142ystok (2007). http:\/\/mizar.org\/trybulec65\/"},{"key":"9440_CR64","doi-asserted-by":"publisher","unstructured":"Naumowicz, A.: SAT-enhanced Mizar proof checking. In: Watt et\u00a0al.[91], pp. 449\u2013452. https:\/\/doi.org\/10.1007\/978-3-319-08434-3_37","DOI":"10.1007\/978-3-319-08434-3_37"},{"key":"9440_CR65","unstructured":"Naumowicz, A.: Teaching how to write a proof. In: FORMED 2008: Formal Methods in Computer Science Education. Budapest, March 29, 2008, pp. 91\u2013100 (2008)"},{"key":"9440_CR66","doi-asserted-by":"publisher","unstructured":"Naumowicz, A.: Tools for MML environment analysis. In: Kerber et\u00a0al. [46], pp. 348\u2013352. https:\/\/doi.org\/10.1007\/978-3-319-20615-8_26","DOI":"10.1007\/978-3-319-20615-8_26"},{"key":"9440_CR67","doi-asserted-by":"publisher","unstructured":"Naumowicz, A.: Towards standardized Mizar environments. In: \u00a0Borzemski, L., \u00a0Swiatek, J., \u00a0Wilimowska, Z. (eds.) Information Systems Architecture and Technology: Proceedings of 38th International Conference on Information Systems Architecture and Technology\u2014ISAT 2017\u2014Part II, Szklarska Por\u0119ba, Poland, September 17\u201319, 2017. Advances in Intelligent Systems and Computing, vol. 656, pp. 166\u2013175. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-67229-8_15","DOI":"10.1007\/978-3-319-67229-8_15"},{"issue":"1","key":"9440_CR68","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 Gr\u00f6bner bases computation in Mizar proof checking. Int. J. Comput. Math. 87(1), 1\u201311 (2010). https:\/\/doi.org\/10.1080\/00207160701864459","journal-title":"Int. J. Comput. Math."},{"issue":"3","key":"9440_CR69","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/s10817-015-9332-6","journal-title":"J. Autom. Reason."},{"key":"9440_CR70","unstructured":"Nowak, B., Trybulec, A.: Hahn-Banach theorem. Formaliz. Math. 4(1), 29\u201334 (1993). http:\/\/fm.mizar.org\/1993-4\/pdf4-1\/hahnban.pdf"},{"key":"9440_CR71","doi-asserted-by":"publisher","unstructured":"P\u0105k, K.: Automated improving of proof legibility in the Mizar system. In: Watt et\u00a0al.[91], pp. 373\u2013387. https:\/\/doi.org\/10.1007\/978-3-319-08434-3_27","DOI":"10.1007\/978-3-319-08434-3_27"},{"issue":"2","key":"9440_CR72","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/s10817-012-9267-0","volume":"50","author":"K P\u0105k","year":"2013","unstructured":"P\u0105k, K.: Methods of lemma extraction in natural deduction proofs. J. Autom. Reason. 50(2), 217\u2013228 (2013). https:\/\/doi.org\/10.1007\/s10817-012-9267-0","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9440_CR73","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s10817-015-9337-1","volume":"55","author":"K P\u0105k","year":"2015","unstructured":"P\u0105k, K.: Improving legibility of formal proofs based on the close reference principle is NP-hard. J. Autom. Reason. 55(3), 295\u2013306 (2015). https:\/\/doi.org\/10.1007\/s10817-015-9337-1","journal-title":"J. Autom. Reason."},{"key":"9440_CR74","unstructured":"Retel, K.: The class of series\u2014parallel graphs. Part I. Formaliz. Math. 11(1), 99\u2013103 (2003). http:\/\/fm.mizar.org\/2003-11\/pdf11-1\/necklace.pdf"},{"issue":"1","key":"9440_CR75","first-page":"35","volume":"4","author":"K Retel","year":"2005","unstructured":"Retel, K., Zalewska, A.: Mizar as a\u00a0tool for teaching mathematics. Mech. Math. Appl. Spec. Issue 30 Years of Mizar 4(1), 35\u201342 (2005)","journal-title":"Mech. Math. Appl. Spec. Issue 30 Years of Mizar"},{"key":"9440_CR76","unstructured":"Rudnicki, P., Trybulec, A.: A collection of TeXed Mizar abstracts. University of Alberta, Techical Report (1989)"},{"key":"9440_CR77","unstructured":"Rudnicki, P., Trybulec, A.: Abian\u2019s fixed point theorem. Formaliz. Math. 6(3), 335\u2013338 (1997). http:\/\/fm.mizar.org\/1997-6\/pdf6-3\/abian.pdf"},{"key":"9440_CR78","unstructured":"Rudnicki, P., Trybulec, A.: Mathematical knowledge management in Mizar. In: Proceedings of MKM 2001 (2001)"},{"issue":"5","key":"9440_CR79","doi-asserted-by":"publisher","first-page":"607","DOI":"10.3233\/AIC-160709","volume":"29","author":"G Sutcliffe","year":"2016","unstructured":"Sutcliffe, G.: The 8th IJCAR automated theorem proving system competition\u2014CASC-J8. AI Commun. 29(5), 607\u2013619 (2016). https:\/\/doi.org\/10.3233\/AIC-160709","journal-title":"AI Commun."},{"key":"9440_CR80","doi-asserted-by":"crossref","first-page":"176","DOI":"10.4064\/fm-32-1-176-783","volume":"32","author":"A Tarski","year":"1939","unstructured":"Tarski, A.: On well-ordered subsets of any set. Fundam. Math. 32, 176\u2013183 (1939)","journal-title":"Fundam. Math."},{"key":"9440_CR81","unstructured":"The QED manifesto. In: Bundy, A. (ed.) CADE. Lecture Notes in Computer Science, vol. 814, pp. 238\u2013251. Springer (1994)"},{"issue":"6","key":"9440_CR82","doi-asserted-by":"crossref","first-page":"2491","DOI":"10.1090\/S0002-9947-99-02400-9","volume":"352","author":"S Thomasse","year":"2000","unstructured":"Thomasse, S.: On better-quasi-ordering countable series-parallel orders. Trans. Am. Math. Soc. 352(6), 2491\u20132505 (2000)","journal-title":"Trans. Am. Math. Soc."},{"key":"9440_CR83","unstructured":"Trybulec, A.: Algebra of normal forms is a Heyting algebra. Formaliz. Math. 2(3), 393\u2013396 (1991). http:\/\/fm.mizar.org\/1991-2\/pdf2-3\/heyting1.pdf"},{"key":"9440_CR84","unstructured":"Trybulec, A.: Algebra of normal forms. Formaliz. Math. 2(2), 237\u2013242 (1991). http:\/\/fm.mizar.org\/1991-2\/pdf2-2\/normform.pdf"},{"key":"9440_CR85","doi-asserted-by":"publisher","unstructured":"Urban, J.: XML-izing Mizar: making semantic processing and presentation of MML easy. In: \u00a0Kohlhase, M. (ed.) Mathematical Knowledge Management, 4th International Conference, MKM 2005, Bremen, Germany, July 15\u201317, 2005, Revised Selected Papers. Lecture Notes in Computer Science, vol. 3863, pp. 346\u2013360. Springer (2005). https:\/\/doi.org\/10.1007\/11618027_23","DOI":"10.1007\/11618027_23"},{"issue":"3\u20134","key":"9440_CR86","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\u2014motivation, implementation, first experiments. J. Autom. Reason. 33(3\u20134), 319\u2013339 (2004). https:\/\/doi.org\/10.1007\/s10817-004-6245-1","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9440_CR87","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1142\/S0218213006002588","volume":"15","author":"J Urban","year":"2006","unstructured":"Urban, J.: MoMM\u2014fast interreduction and retrieval in large libraries of formalized mathematics. Int. J. Artif. Intell. Tools 15(1), 109\u2013130 (2006). https:\/\/doi.org\/10.1142\/S0218213006002588","journal-title":"Int. J. Artif. Intell. Tools"},{"issue":"1\u20132","key":"9440_CR88","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s10817-006-9032-3","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). https:\/\/doi.org\/10.1007\/s10817-006-9032-3","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9440_CR89","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). https:\/\/doi.org\/10.1007\/s11786-008-0053-7","journal-title":"Math. Comput. Sci."},{"issue":"2","key":"9440_CR90","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). https:\/\/doi.org\/10.1007\/s10817-012-9269-y","journal-title":"J. Autom. Reason."},{"key":"9440_CR91","doi-asserted-by":"publisher","unstructured":"Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.): Intelligent Computer Mathematics\u2014International Conference, CICM 2014, Coimbra, Portugal, July 7\u201311, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8543. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08434-3","DOI":"10.1007\/978-3-319-08434-3"},{"key":"9440_CR92","unstructured":"Wiedijk, F.: Estimating the cost of a standard library for a mathematical proof checker (2001). http:\/\/www.cs.ru.nl\/~freek\/notes\/mathstdlib2.pdf"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-017-9440-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9440-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9440-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,27]],"date-time":"2025-06-27T14:19:38Z","timestamp":1751033978000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-017-9440-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11,25]]},"references-count":92,"journal-issue":{"issue":"1-4","published-print":{"date-parts":[[2018,6]]}},"alternative-id":["9440"],"URL":"https:\/\/doi.org\/10.1007\/s10817-017-9440-6","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,11,25]]}}}