Mizar: state-of-the-art and beyond. (English) Zbl 1417.68201

Kerber, Manfred (ed.) et al., Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9150, 261-279 (2015).
Summary: Mizar is one of the pioneering systems for mathematics formalization, which still has an active user community. The project has been in constant development since 1973, when Andrzej Trybulec designed the fundamentals of a language capable of rigorously encoding mathematical knowledge in a computerized environment which guarantees its full logical correctness. Since then, the system with its feature-rich language devised to approximate mathematics writing has influenced other formalization projects and has given rise to a number of Mizar modes implemented on top of other systems. However, the information about the system as a whole is not readily available to developers of other systems. Various papers describing Mizar features have been rather incremental and focused only on particular newly implemented Mizar aspects. The objective of the current paper is to give a survey of the most important Mizar features that distinguish it from other popular proof checkers. We also go a step further and describe most important current trends and lines of development that go beyond the state-of-the-art system.
For the entire collection see [Zbl 1316.68015].


68T30 Knowledge representation
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI


[1] 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–277. Springer, Heidelberg (2011). http://dx.doi.org/10.1007/978-3-642-22673-1_19 · Zbl 1335.68255
[2] 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–1 July 2012. EPiC Series, vol. 21, pp. 3–11. EasyChair (2012). http://www.easychair.org/publications/?page=1559779348
[3] Alama, J.: Eliciting implicit assumptions of Mizar proofs by property omission. J. Autom. Reasoning 50(2), 123–133 (2013). http://dx.doi.org/ 10.1007/s10817-012-9264-3 · Zbl 1260.68361
[4] 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–148. Springer, Heidelberg (2011). http://dx.doi.org/10.1007/978-3-642-22673-1 · Zbl 1335.68220
[5] 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–163. Springer, Heidelberg (2011). http://dx.doi.org/10.1007/978-3-642-22673-1_11 · Zbl 1278.68290
[6] 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–16. Springer, Heidelberg (2012). http://dx.doi.org/ 10.1007/978-3-642-31374-5_1 · Zbl 1335.68221
[7] Anonymous: the QED manifesto. Bundy, A. (ed.) CADE 1994. LNCS, vol. 814. Springer, Heidelberg (1994)
[8] Strotmann, A.: The categorial type of OpenMath objects. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 378–392. Springer, Heidelberg (2004) · Zbl 1108.68604
[9] Bancerek, G.: Automatic translation in formalized mathematics. Mech. Math. Appl. 5(2), 19–31 (2006)
[10] 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–279. Springer, Heidelberg (2006). http://dx.doi.org/10.1007/11812289_21 · Zbl 1188.68125
[11] Bancerek, G., Rudnicki, P.: A compendium of continuous lattices in Mizar: formalizing recent mathematics. J. Autom. Reason. 29(3–4), 189–224 (2002) · Zbl 1064.68082
[12] Bancerek, G., Rudnicki, P.: Information retrieval in MML. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol. 2594, pp. 119–132. Springer, Heidelberg (2003) · Zbl 1022.68610
[13] 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–57. Springer, Heidelberg (2004) · Zbl 1108.68583
[14] 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–431. Springer, Heidelberg (2012) · Zbl 1360.68743
[15] 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–72. Springer, Heidelberg (2004) · Zbl 1108.68584
[16] 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–84. Springer, Heidelberg (2008). http://dx.doi.org/10.1007/978-3-540-68103-8_5 · Zbl 1138.68525
[17] 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–286. Springer, Heidelberg (2011) · Zbl 1335.68225
[18] 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–172 (2013). http://dx.doi.org/10.1007/s10817-012-9265-2 · Zbl 1260.68371
[19] 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łystok, vol. 10(23), pp. 249–263 (2007). http://mizar.org/trybulec65/
[20] Grabowski, A.: Efficient rough set theory merging. Fundamenta Informaticae 135(4), 371–385 (2014). http://dx.doi.org/10.3233/FI-2014-1129 · Zbl 1329.68247
[21] Grabowski, A., Korniłowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formaliz. Reason. Spec. Issue: User Tutor. I 3(2), 153–245 (2010) · Zbl 1211.68369
[22] Grabowski, A., Schwarzweller, C.: Translating mathematical vernacular into knowledge repositories. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol. 3863, pp. 49–64. Springer, Heidelberg (2006). http://dx.doi.org/10.1007/11618027_4 · Zbl 1151.68663
[23] 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–249. Springer, Heidelberg (2007). http://dx.doi.org/10.1007/978-3-540-73086-6_20 · Zbl 1202.68465
[24] 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–12 September 2012, pp. 63–68 (2012)
[25] 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
[26] Iancu, M., Kohlhase, M., Rabe, F., Urban, J.: The Mizar mathematical library in OMDoc: translation and applications. J. Autom. Reason. 50(2), 191–202 (2013). http://dx.doi.org/10.1007/s10817-012-9271-4 · Zbl 1260.68375
[27] Jaśkowski, S.: On the Rules of Suppositions in Formal Logic. Studia Logica, Nakładem Seminarjum Filozoficznego Wydziału Matematyczno-Przyrodniczego Uniwersytetu Warszawskiego (1934). http://books.google.pl/books?id=6w0vRAAACAAJ · JFM 60.0846.02
[28] Kaliszyk, C., Urban, J.: MizAR 40 for Mizar 40 (2013). CoRR abs/1310.2805 · Zbl 1356.68191
[29] Kaliszyk, C., Urban, J., Vyskočil, J.: Machine learner for automated reasoning 0.4 and 0.5 (2014). Accepted to PAAR 2014, CoRR abs/1402.2359
[30] Korniłowicz, A.: Jordan curve theorem. Formaliz. Math. 13(4), 481–491 (2005)
[31] Korniłowicz, A.: On rewriting rules in Mizar. J. Autom. Reason. 50(2), 203–210 (2013). http://dx.doi.org/10.1007/s10817-012-9261-6 · Zbl 1260.68376
[32] 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–24 (2005)
[33] Naumowicz, A.: An example of formalizing recent mathematical results in Mizar. J. Appl. Logic 4(4), 396–413 (2006). http://www.sciencedirect.com/ science/article/pii/S1570868305000686 · Zbl 1107.68100
[34] 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łystok, vol. 18, no. 31, pp. 89–101 (2009)
[35] Naumowicz, A.: Interfacing external CA systems for Grobner bases computation in Mizar proof checking. Int. J. Comput. Math. 87(1), 1–11 (2010). http://dx.doi.org/10.1080/00207160701864459 · Zbl 1178.68692
[36] 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–452. Springer, Heidelberg (2014). http://dx.doi.org/10.1007/ 978-3-319-08434-3_37 · Zbl 1304.68159
[37] Naumowicz, A., Byliński, C.: Improving Mizar texts with properties and requirements. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 290–301. Springer, Heidelberg (2004). http://dx.doi.org/ 10.1007/978-3-540-27818-4_21 · Zbl 1108.68598
[38] Naumowicz, A., Korniłowicz, A.: A brief overview of Mizar. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 67–72. Springer, Heidelberg (2009). http://dx.doi.org/10.1007/978-3-642-03359-9_5 · Zbl 1252.68262
[39] Pąk, K.: Methods of lemma extraction in natural deduction proofs. J. Autom. Reason. 50(2), 217–228 (2013). http://dx.doi.org/10.1007/s10817-012-9267-0 · Zbl 1260.68379
[40] Pąk, K.: Improving legibility of natural deduction proofs is not trivial. Logic. Methods Comput. Sci. 10(3), 1–30 (2014). http://dx.doi.org/10.2168/ LMCS-10(3:23)2014
[41] 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–174. Springer, Heidelberg (2003) · Zbl 1022.68621
[42] Syme, D.: DECLARE: a prototype declarative proof system for higher order logic. Technical report, University of Cambridge (1997)
[43] Trybulec, A., Korniłowicz, A., Naumowicz, A., Kuperberg, K.: Formal mathematics for mathematicians. J. Autom. Reason. 50(2), 119–121 (2013). http://dx.doi.org/ 10.1007/s10817-012-9268-z
[44] Urban, J., Sutcliffe, G., Trac, S., Puzis, Y.: Combining Mizar and TPTP semantic presentation and verification tools. Stud. Logic Gramm. Rhetor. 18(31), 121–136 (2009)
[45] Urban, J.: MPTP - motivation, implementation, first experiments. J. Autom. Reason. 33(3–4), 319–339 (2004) · Zbl 1075.68081
[46] 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–360. Springer, Heidelberg (2006) · Zbl 1151.68681
[47] Urban, J.: MizarMode – an integrated proof assistance tool for the Mizar way of formalizing mathematics. J. Appl. Logic 4(4), 414–427 (2006). http://dx.doi.org/ 10.1016/j.jal.2005.10.004 · Zbl 1107.68103
[48] Urban, J.: MoMM – fast interreduction and retrieval in large libraries of formalized mathematics. Int. J. Artif. Intell. Tools 15(1), 109–130 (2006). http://ktiml.mff.cuni.cz/urban/MoMM/momm.ps · Zbl 05421611
[49] Urban, J.: MPTP 0.2: design, implementation, and initial experiments. J. Autom. Reason. 37(1–2), 21–43 (2006). http://dx.doi.org/10.1007/s10817-006-9032-3 · Zbl 1113.68095
[50] Urban, J.: BliStr: The Blind Strategymaker (2014). Accepted to PAAR 2014, CoRR abs/1301.2683
[51] 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–469. Springer, Heidelberg (2010) · Zbl 1286.68434
[52] Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. J. Autom. Reason. 50(2), 229–241 (2013). http://dx.doi.org/10.1007/ s10817-012-9269-y · Zbl 1260.68380
[53] Urban, J., Sutcliffe, G.: ATP-based cross-verification of Mizar proofs: method, systems, and first experiments. Math. Comput. Sci. 2(2), 231–251 (2008). http://dx.doi.org/10.1007/s11786-008-0053-7 · Zbl 1178.68532
[54] Urban, J., Sutcliffe, G., Pudlák, P., Vyskočil, 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–456. Springer, Heidelberg (2008) · Zbl 1165.68434
[55] Urban, J., Vyskočil, J., Štěpánek, P.: MaLeCoP machine learning connection prover. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS, vol. 6793, pp. 263–277. Springer, Heidelberg (2011) · Zbl 1332.68206
[56] Wenzel, M., Wiedijk, F.: A comparison of Mizar and Isar. J. Autom. Reason. 29(3–4), 389–411 (2003). http://dx.doi.org/10.1023/A:1021935419355 · Zbl 1064.68083
[57] Wiedijk, F.: Mizar light for HOL light. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 378–394. Springer, Heidelberg (2001) · Zbl 1005.68539
[58] Wiedijk, F.: Formal proof sketches. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 378–393. Springer, Heidelberg (2004) · Zbl 1100.68620
[59] Gamboa, R.: ACL2. In: Wiedijk, F. (ed.) The Seventeen Provers of the World. LNCS (LNAI), vol. 3600, pp. 55–66. Springer, Heidelberg (2006)
[60] Wiedijk, F.: Formal proof–getting started. Not. Am. Math. Soc. 55(11), 1408–1414 (2008) · Zbl 1188.68267
[61] Wiedijk, F.: A synthesis of the procedural and declarative styles of interactive theorem proving. Logic. Methods Comput. Sci. 8(1:30), 1–26 (2012) · Zbl 1238.68147
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.