×

The role of the Mizar mathematical library for interactive proof development in Mizar. (English) Zbl 1433.68530

Summary: The Mizar system is one of the pioneering systems aimed at supporting mathematical proof development on a computer that have laid the groundwork for and eventually have evolved into modern interactive proof assistants. We claim that an important milestone in the development of these systems was the creation of organized libraries accumulating all previously available formalized knowledge in such a way that new works could effectively re-use all previously collected notions. In the case of Mizar, the turning point of its development was the decision to start building the Mizar Mathematical Library as a centrally-managed knowledge base maintained together with the formalization language and the verification system. In this paper we show the process of forming this library, the evolution of its design principles, and also present some data showing its current use with the modern version of the Mizar proof checker, but also as a rich corpus of semantically linked mathematical data in various areas including web-based and natural language proof presentation, maths education, and machine learning based automated theorem proving.

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
68V20 Formalization of mathematics in connection with theorem provers
68V30 Mathematical knowledge management
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abad, P., Abad, J.: The hundred greatest theorems (1999). http://www.cs.ru.nl/ freek/100/
[2] Adams, A.A., Davenport, J.H.: Copyright issues for MKM. In: Asperti et al. [7], pp. 1-16. https://doi.org/10.1007/978-3-540-27818-4_1 · Zbl 1108.68581
[3] Alama, J., Brink, K., Mamane, L., Urban, J.: Large formal wikis: issues and solutions. In: Davenport et al. [19], pp. 133-148. https://doi.org/10.1007/978-3-642-22673-1_10 · Zbl 1335.68220
[4] 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.) Proceedings of the 18th Calculemus and 10th International Conference on Intelligent Computer Mathematics. MKM’11, Lecture Notes in Computer Science, vol. 6824, pp. 149-163. Springer, Berlin, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22673-1_11 · Zbl 1278.68290
[5] Alama, J., Mamane, L., Urban, J.: Dependencies in formal mathematics: applications and extraction for Coq and Mizar. In: Jeuring, J., Campbell, J.A., Carette, J., Reis, G.D., Sojka, P., Wenzel, M., Sorge, V. (eds.) Intelligent Computer Mathematics—11th 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-13, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7362, pp. 1-16. Springer (2012). https://doi.org/10.1007/978-3-642-31374-5_1
[6] Alama, J.: Mizar-items: exploring fine-grained dependencies in the Mizar mathematical library. In: Davenport et al. [19], pp. 276-277. https://doi.org/10.1007/978-3-642-22673-1_19 · Zbl 1335.68255
[7] Asperti, A., Bancerek, G., Trybulec, A. (eds.): Mathematical Knowledge Management. In: Proceedings of Third International Conference, MKM 2004, Bialowieza, Poland, September 19-21, 2004, Lecture Notes in Computer Science, vol. 3119. Springer (2004) · Zbl 1053.68003
[8] Aspinall, D., Kaliszyk, C.: Towards formal proof metrics. In: Stevens, P., Wasowski, A. (eds.) 19th International Conference on Fundamental Approaches to Software Engineering (FASE 2016). Lecture Notes in Computer Science, vol. 9633, pp. 325-341. Springer (2016). https://doi.org/10.1007/978-3-662-49665-7_19 · Zbl 1260.68380
[9] Bancerek, G., Byliński, C., Grabowski, A., Korniłowicz, A., Matuszewski, R., Naumowicz, A., Pąk, K., Urban, J.: Mizar: State-of-the-art and beyond. In: Kerber et al. [46], pp. 261-279. https://doi.org/10.1007/978-3-319-20615-8_17 · Zbl 1417.68201
[10] Bancerek, G., Hryniewiecki, K.: Segments of natural numbers and finite sequences. Formalized Math 1(1), 107-114 (1990). http://fm.mizar.org/1990-1/pdf1-1/finseq_1.pdf · Zbl 1113.68095
[11] Bancerek, G.: Information retrieval and rendering with MML Query. In: J. Borwein, W. Farmer (eds.) Mathematical Knowledge Management. Lecture Notes in Computer Science, vol. 4108, pp. 266-279. Springer, Berlin Heidelberg (2006). https://doi.org/10.1007/11812289_21 · Zbl 1188.68125
[12] Bancerek, G, Automatic translation in formalized mathematics, Mech. Math. Appl., 5, 19-31, (2006)
[13] Bancerek, G; Rudnicki, P, A compendium of continuous lattices in mizar: formalizing recent mathematics, J. Autom. Reason., 29, 189-224, (2002) · Zbl 1064.68082
[14] Blanchette, J.C., Haslbeck, M., Matichuk, D., Nipkow, T.: Mining the archive of formal proofs. In: Kerber et al. [46], pp. 3-17. https://doi.org/10.1007/978-3-319-20615-8_1 · Zbl 1417.68176
[15] Blanchette, JC; Kaliszyk, C; Paulson, LC; Urban, J, Hammering towards QED, J. Formaliz. Reason., 9, 101-148, (2016)
[16] Borak, E., Zalewska, A.: Mizar Course in Logic and Set Theory, pp. 191-204. Springer Berlin Heidelberg, Berlin, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73086-6_17 · Zbl 1202.68373
[17] Borsuk, K, On the homotopy types of some decomposition spaces, Bull. Acad. Polon. Sci., 18, 235-239, (1970) · Zbl 0194.55004
[18] Butler, R.W., Sjogren, J.A.: A PVS graph theory library. Technical Report (1998) · JFM 65.1165.01
[19] 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-23, 2011. Proceedings, Lecture Notes in Computer Science, vol. 6824. Springer (2011). https://doi.org/10.1007/978-3-642-22673-1 · Zbl 1218.68014
[20] de Bruijn, 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-61. Springer LNM 125, Versailles, France (1968)
[21] Gauthier, T., Kaliszyk, C., Urban, J.: Initial experiments with statistical conjecturing over large formal corpora. In: Kohlhase, A., Libbrecht P., Miller, B.R., Naumowicz, A., Neuper, W., Quaresma, 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-29, 2016. CEUR Workshop Proceedings, vol. 1785, pp. 219-228. CEUR-WS.org (2016). http://ceur-ws.org/Vol-1785/W23.pdf
[22] Gauthier, T., Kaliszyk, C.: Aligning concepts across proof assistant libraries. J. Symbol. Comput. (to appear) (2017) · Zbl 1395.68247
[23] Gierz, G., Hofmann, K., Keimel, K., Lawson, J., Mislove, M., Scott, D.: A Compendium of Continuous Lattices. Springer, Berlin, Heidelberg, New York (1980) · Zbl 0452.06001
[24] 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) · Zbl 1088.06001
[25] Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Roux, S.L., Mahboubi, A., O’Connor, R., Biha, S.O., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Théry, L.: A machine-checked proof of the Odd Order Theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP. Lecture Notes in Computer Science, vol. 7998, pp. 163-179. Springer (2013) · Zbl 1317.68211
[26] Grabowski, A., Korniłowicz, A., Schwarzweller, C.: Equality in computer proof-assistants. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Proceedings of the 2015 Federated Conference on Computer Science and Information Systems. Annals of Computer Science and Information Systems, vol. 5, pp. 45-54. IEEE (2015). https://doi.org/10.15439/2015F229 · Zbl 1260.68379
[27] Grabowski, A., Korniłowicz, A., Schwarzweller, C.: On algebraic hierarchies in mathematical repository of Mizar. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Proceedings of the 2016 Federated Conference on Computer Science and Information Systems. Annals of Computer Science and Information Systems, vol. 8, pp. 363-371. IEEE (2016). https://doi.org/10.15439/2016F520
[28] Grabowski, A., Moschner, M.: Managing heterogeneous theories within a mathematical knowledge repository. In: Asperti et al. [7], pp. 116-129. https://doi.org/10.1007/978-3-540-27818-4_9 · Zbl 1108.68589
[29] Grabowski, A., Schwarzweller, C.: On duplication in mathematical repositories. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, 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-10, 2010. Proceedings, Lecture Notes in Computer Science, vol. 6167, pp. 300-314. Springer (2010). https://doi.org/10.1007/978-3-642-14128-7_26 · Zbl 1356.68197
[30] 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 ’07 / MKM ’07, pp. 235-249. Springer-Verlag, Berlin, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73086-6_20 · Zbl 1202.68465
[31] Grabowski, A.: Expressing the notion of a mathematical structure in the formal language of Mizar. In: Gruca, A., Czachorski, T., Harezlak, K., Kozielski, S., Piotrowska, A. (eds.) Man-Machine Interactions 5. ICMMI 2017, vol. 659, pp. 261-270. Springer (2017). https://doi.org/10.1007/978-3-319-67792-7_26
[32] Grabowski, A, Mechanizing complemented lattices within mizar type system, J. Autom. Reason., 55, 211-221, (2015) · Zbl 1356.68189
[33] Grabowski, A, Lattice theory for rough sets—a case study with mizar, Fundam. Inform., 147, 223-240, (2016) · Zbl 1419.68164
[34] Grabowski, A; Korniłowicz, A; Naumowicz, A, Mizar in a nutshell, J. Formaliz. Reason., 3, 153-245, (2010) · Zbl 1211.68369
[35] Grabowski, A., Korniłowicz, A., Naumowicz, A.: Four decades of Mizar. J. Autom. Reason. 55(3), 191-198 (2015). https://doi.org/10.1007/s10817-015-9345-1 · Zbl 1336.00111
[36] Hales, T., Adams, M., Bauer, G., Dang, T.D., Harrison, J., Hoang, L.T., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T., et al.: A formal proof of the Kepler conjecture. Forum of Mathematics, Pi 5 (2017). https://doi.org/10.1017/fmp.2017.1 · Zbl 1379.52018
[37] Iancu, M; Kohlhase, M; Rabe, F; Urban, J, The mizar mathematical library in omdoc: translation and applications, J. Autom. Reason., 50, 191-202, (2013) · Zbl 1260.68375
[38] Irving, G., Szegedy, C., Alemi, A.A., Eén, N., Chollet, F., Urban, J.: Deepmath—deep sequence models for premise selection. In: Lee, D.D., Sugiyama, M., von Luxburg, U., Guyon, I., Garnett, R. (eds.) Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016, December 5-10, 2016, Barcelona, Spain, pp. 2235-2243 (2016). http://papers.nips.cc/paper/6280-deepmath-deep-sequence-models-for-premise-selection
[39] Kaliszyk, C., Pąk, K., Urban, J.: Towards a Mizar environment for Isabelle: foundations and language. In: Avigad, J., Chlipala, A. (eds.) Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016, pp. 58-65. ACM (2016). https://doi.org/10.1145/2854065.2854070
[40] Kaliszyk, C., Schulz, S., Urban, J., Vyskočil, J.: System description: E.T. 0.1. In: Felty, A.P., Middeldorp, A. (eds.) Proceedings of 25th International Conference on Automated Deduction (CADE’15). LNCS, vol. 9195, pp. 389-398. Springer (2015). https://doi.org/10.1007/978-3-319-21401-6_27 · Zbl 1465.68286
[41] Kaliszyk, C., Urban, J., Vyskočil, J.: Efficient semantic features for automated reasoning over large theories. In: Yang, Q., Wooldridge, M. (eds.) Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI’15), pp. 3084-3090. AAAI Press (2015) · Zbl 1371.68003
[42] Kaliszyk, C., Urban, J., Vyskočil, J.: Lemmatization for stronger reasoning in large theories. In: Lutz, C., Ranise, S. (eds.) Frontiers of Combining Systems (FroCoS’15). LNCS, vol. 9322, pp. 341-356. Springer (2015). https://doi.org/10.1007/978-3-319-24246-0_21 · Zbl 1471.68313
[43] Kaliszyk, C., Urban, J., Vyskočil, J.: System description: Statistical parsing of informalized Mizar formulas (to appear) (2017) · Zbl 1356.68192
[44] Kaliszyk, C; Urban, J, Learning-assisted theorem proving with millions of lemmas, J. Symbol. Comput., 69, 109-128, (2015) · Zbl 1315.68220
[45] Kaliszyk, C; Urban, J, Mizar 40 for mizar 40, J. Autom. Reason., 55, 245-256, (2015) · Zbl 1356.68191
[46] Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.): Intelligent Computer Mathematics—International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings, Lecture Notes in Computer Science, vol. 9150. Springer (2015). https://doi.org/10.1007/978-3-319-20615-8 · Zbl 1316.68015
[47] 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’09, pp. 207-220. ACM, New York, NY, USA (2009). https://doi.org/10.1145/1629575.1629596
[48] Kohlhase, M., Johansson, M., Miller, B.R., de Moura, L., Tompa, F.W. (eds.): Intelligent Computer Mathematics. In: Proceedings of the 9th International Conference, CICM 2016, Bialystok, Poland, July 25-29, 2016, Lecture Notes in Computer Science, vol. 9791. Springer (2016). https://doi.org/10.1007/978-3-319-42547-4 · Zbl 1342.68025
[49] Korniłowicz, A.: Enhancement of Mizar texts with transitivity property of predicates. In: Kohlhase et al. [48], pp. 157-162. https://doi.org/10.1007/978-3-319-42547-4_12 · Zbl 1344.68206
[50] Korniłowicz, A, A proof of the Jordan curve theorem via the Brouwer fixed point theorem, Mech. Math. Appl. Spe. Issue Jordan Curve Theorem, 6, 33-40, (2007)
[51] Korniłowicz, A, On rewriting rules in mizar, J. Autom. Reason., 50, 203-210, (2013) · Zbl 1260.68376
[52] Korniłowicz, A, Definitional expansions in mizar, J. Autom. Reason., 55, 257-268, (2015) · Zbl 1356.68192
[53] Korniłowicz, A, Flexary connectives in mizar, Comput. Lang. Syst. Struct., 44, 238-250, (2015) · Zbl 1387.68207
[54] Letichevsky, AA; Lyaletski, AV; Morokhovets, MK, Glushkov’s evidence algorithm, Cybern. Syst. Anal., 49, 489-500, (2013) · Zbl 1371.68003
[55] Loos, S., Irving, G., Szegedy, C., Kaliszyk, C.: Deep network guided proof search. In: Eiter, T., Sands, D. (eds.) LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol. 46, pp. 85-105. EasyChair (2017)
[56] Matuszewski, R; Rudnicki, P, Mizar: the first 30 years, Mech. Math. Appl. Special Issue on 30 Years of Mizar, 4, 3-24, (2005)
[57] Milewski, R.: Fundamental theorem of algebra. Formaliz. Math. 9(3), 461-470 (2001). http://fm.mizar.org/2001-9/pdf9-3/polynom5.pdf
[58] Milner, R, Implementation and applications of scott’s logic for computable functions, SIGPLAN Not., 7, 1-6, (1972)
[59] Naumowicz, A., Byliński, C.: Improving Mizar texts with properties and requirements. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) Mathematical Knowledge Management, Third International Conference, MKM 2004 Proceedings. MKM’04, Lecture Notes in Computer Science, vol. 3119, pp. 290-301 (2004). https://doi.org/10.1007/978-3-540-27818-4_21 · Zbl 1108.68598
[60] Naumowicz, A., Korniłowicz, A.: Introducing Euclidean relations to Mizar. In: Ganzha, M., Maciaszek, L.A., Paprzycki,M. (eds.) Proceedings of the 2017 Federated Conference on Computer Science and Information Systems, FedCSIS 2017, Prague, Czech Republic, September 3-6, 2017. Annals of Computer Science and Information Systems, vol. 11, pp. 245-248. IEEE (2017). https://doi.org/10.15439/2017F368
[61] Naumowicz, A., Piliszek, R.: Accessing the Mizar library with a weakly strict Mizar parser. In: Kohlhase et al. [48], pp. 77-82. https://doi.org/10.1007/978-3-319-42547-4_6 · Zbl 1344.68211
[62] 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, vol. 18(31), pp. 89-101. University of Białystok (2009) · Zbl 1356.68189
[63] Naumowicz, A.: Evaluating prospective built-in elements of computer algebra in Mizar. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar and Rhetoric, vol. 10(23), pp. 191-200. University of Białystok (2007). http://mizar.org/trybulec65/
[64] Naumowicz, A.: SAT-enhanced Mizar proof checking. In: Watt et al.[91], pp. 449-452. https://doi.org/10.1007/978-3-319-08434-3_37 · Zbl 1304.68159
[65] Naumowicz, A.: Teaching how to write a proof. In: FORMED 2008: Formal Methods in Computer Science Education. Budapest, March 29, 2008, pp. 91-100 (2008)
[66] Naumowicz, A.: Tools for MML environment analysis. In: Kerber et al. [46], pp. 348-352. https://doi.org/10.1007/978-3-319-20615-8_26 · Zbl 1417.68213
[67] Naumowicz, A.: Towards standardized Mizar environments. In: Borzemski, L., Swiatek, J., Wilimowska, Z. (eds.) Information Systems Architecture and Technology: Proceedings of 38th International Conference on Information Systems Architecture and Technology—ISAT 2017—Part II, Szklarska Poręba, Poland, September 17-19, 2017. Advances in Intelligent Systems and Computing, vol. 656, pp. 166-175. Springer (2017). https://doi.org/10.1007/978-3-319-67229-8_15
[68] Naumowicz, A, Interfacing external CA systems for Gröbner bases computation in mizar proof checking, Int. J. Comput. Math., 87, 1-11, (2010) · Zbl 1178.68692
[69] Naumowicz, A, Automating Boolean set operations in mizar proof checking with the aid of an external SAT solver, J. Autom. Reason., 55, 285-294, (2015) · Zbl 1356.68197
[70] Nowak, B., Trybulec, A.: Hahn-Banach theorem. Formaliz. Math. 4(1), 29-34 (1993). http://fm.mizar.org/1993-4/pdf4-1/hahnban.pdf
[71] Pąk, K.: Automated improving of proof legibility in the Mizar system. In: Watt et al.[91], pp. 373-387. https://doi.org/10.1007/978-3-319-08434-3_27 · Zbl 1304.68160
[72] Pąk, K, Methods of lemma extraction in natural deduction proofs, J. Autom. Reason., 50, 217-228, (2013) · Zbl 1260.68379
[73] Pąk, K, Improving legibility of formal proofs based on the close reference principle is NP-hard, J. Autom. Reason., 55, 295-306, (2015) · Zbl 1356.68198
[74] Retel, K.: The class of series—parallel graphs. Part I. Formaliz. Math. 11(1), 99-103 (2003). http://fm.mizar.org/2003-11/pdf11-1/necklace.pdf
[75] Retel, K; Zalewska, A, Mizar as a tool for teaching mathematics, Mech. Math. Appl. Spec. Issue 30 Years of Mizar, 4, 35-42, (2005)
[76] Rudnicki, P., Trybulec, A.: A collection of TeXed Mizar abstracts. University of Alberta, Techical Report (1989) · Zbl 0194.55004
[77] Rudnicki, P., Trybulec, A.: Abian’s fixed point theorem. Formaliz. Math. 6(3), 335-338 (1997). http://fm.mizar.org/1997-6/pdf6-3/abian.pdf
[78] Rudnicki, P., Trybulec, A.: Mathematical knowledge management in Mizar. In: Proceedings of MKM 2001 (2001) · Zbl 0982.68136
[79] Sutcliffe, G, The 8th IJCAR automated theorem proving system competition—CASC-J8, AI Commun., 29, 607-619, (2016) · Zbl 1373.68367
[80] Tarski, A, On well-ordered subsets of any set, Fundam. Math., 32, 176-183, (1939) · Zbl 0021.11003
[81] The QED manifesto. In: Bundy, A. (ed.) CADE. Lecture Notes in Computer Science, vol. 814, pp. 238-251. Springer (1994)
[82] Thomasse, S, On better-quasi-ordering countable series-parallel orders, Trans. Am. Math. Soc., 352, 2491-2505, (2000) · Zbl 0944.05052
[83] Trybulec, A.: Algebra of normal forms is a Heyting algebra. Formaliz. Math. 2(3), 393-396 (1991). http://fm.mizar.org/1991-2/pdf2-3/heyting1.pdf
[84] Trybulec, A.: Algebra of normal forms. Formaliz. Math. 2(2), 237-242 (1991). http://fm.mizar.org/1991-2/pdf2-2/normform.pdf
[85] Urban, J.: XML-izing Mizar: making semantic processing and presentation of MML easy. In: Kohlhase, M. (ed.) Mathematical Knowledge Management, 4th International Conference, MKM 2005, Bremen, Germany, July 15-17, 2005, Revised Selected Papers. Lecture Notes in Computer Science, vol. 3863, pp. 346-360. Springer (2005). https://doi.org/10.1007/11618027_23 · Zbl 1151.68681
[86] Urban, J, MPTP—motivation, implementation, first experiments, J. Autom. Reason., 33, 319-339, (2004) · Zbl 1075.68081
[87] Urban, J, Momm—fast interreduction and retrieval in large libraries of formalized mathematics, Int. J. Artif. Intell. Tools, 15, 109-130, (2006)
[88] Urban, J, MPTP 0.2: design, implementation, and initial experiments, J. Autom. Reason., 37, 21-43, (2006) · Zbl 1113.68095
[89] Urban, J; Sutcliffe, G, ATP-based cross-verification of mizar proofs: method, systems, and first experiments, Math. Comput. Sci., 2, 231-251, (2008) · Zbl 1178.68532
[90] Urban, J; Rudnicki, P; Sutcliffe, G, ATP and presentation service for mizar formalizations, J. Autom. Reason., 50, 229-241, (2013) · Zbl 1260.68380
[91] Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.): Intelligent Computer Mathematics—International Conference, CICM 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8543. Springer (2014). https://doi.org/10.1007/978-3-319-08434-3 · Zbl 1293.68035
[92] Wiedijk, F.: Estimating the cost of a standard library for a mathematical proof checker (2001). http://www.cs.ru.nl/ freek/notes/mathstdlib2.pdf
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.