Semantics of Mizar as an Isabelle object logic. (English) Zbl 1468.68290

Summary: We formally define the foundations of the Mizar system as an object logic in the Isabelle logical framework. For this, we propose adequate mechanisms to represent the various components of Mizar. We express Mizar types in a uniform way, provide a common type intersection operation, allow reasoning about type inhabitation, and develop a type inference mechanism. We provide Mizar-like definition mechanisms which require the same proof obligations and provide same derived properties. Structures and set comprehension operators can be defined as definitional extensions. Re-formalized proofs from various parts of the Mizar Library show the practical usability of the specified foundations.


68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
03B35 Mechanization of proofs and logical operations
Full Text: DOI


[1] Abrial, J.: Modeling in Event-B—System and Software Engineering. Cambridge University Press, Cambridge (2010) · Zbl 1213.68214
[2] Adams, M., Proof auditing formalised mathematics, J. Formaliz. Reason., 9, 3-32, (2016)
[3] Agerholm, S.; Gordon, MJC; Schubert, ET (ed.); Windley, PJ (ed.); Alves-Foss, J. (ed.), Experiments with ZF set theory in HOL and Isabelle, 32-45, (1995), Berlin · Zbl 1063.68641
[4] Alama, J.; Heskes, T.; Kühlwein, D.; Tsivtsivadze, E.; Urban, J., Premise selection for mathematics by corpus analysis and kernel methods, J. Autom. Reason., 52, 191-213, (2014) · Zbl 1315.68217
[5] Asperti, A., Bancerek, G., Trybulec, A. (eds.): Mathematical Knowledge Management (MKM 2004), Volume 3119 of LNCS. Springer, Berlin (2004)
[6] Bancerek, G., Tarski’s classes and ranks, Formaliz. Math., 1, 563-567, (1990)
[7] Bancerek, G.; Byliński, C.; Grabowski, A.; Korniłowicz, A.; Matuszewski, R.; Naumowicz, A.; Pąk, K., The role of the Mizar Mathematical Library for interactive proof development in Mizar, J. Autom. Reason., (2017) · Zbl 1433.68530
[8] Bancerek, G.; Byliński, C.; Grabowski, A.; Korniłowicz, A.; Matuszewski, R.; Naumowicz, A.; Pąk, K.; Urban, J.; Kerber, M. (ed.); Carette, J. (ed.); Kaliszyk, C. (ed.); Rabe, F. (ed.); Sorge, V. (ed.), Mizar: state-of-the-art and beyond, 261-279, (2015), Berlin
[9] Bancerek, G.; Rudnicki, P., A compendium of continuous lattices in MIZAR, J. Autom. Reason., 29, 189-224, (2002) · Zbl 1064.68082
[10] Bancerek, G.; Rudnicki, P.; Asperti, A. (ed.); Buchberger, B. (ed.); Davenport, JH (ed.), Information retrieval in MML, 119-132, (2003), Berlin · Zbl 1022.68610
[11] Bancerek, G.; Urban, J.; Asperti, A. (ed.); Bancerek, G. (ed.); Trybulec, A. (ed.), Integrated semantic browsing of the Mizar Mathematical Library for authoring Mizar articles, 44-57, (2004), Berlin · Zbl 1108.68583
[12] Barras, B.; Tankink, C.; Tassi, E.; Urban, C. (ed.); Zhang, X. (ed.), Asynchronous processing of Coq documents: from the kernel up to the user interface, 51-66, (2015), Berlin · Zbl 1465.68275
[13] Blanchette, JC; Greenaway, D.; Kaliszyk, C.; Kühlwein, D.; Urban, J., A learning-based fact selector for Isabelle/HOL, J. Autom. Reason., 57, 219-244, (2016) · Zbl 1386.68149
[14] Blanchette, JC; Nipkow, T.; Kaufmann, M. (ed.); Paulson, LC (ed.), Nitpick: a counterexample generator for higher-order logic based on a relational model finder, 131-146, (2010), Berlin · Zbl 1291.68326
[15] Brown, C.E.: The Egal Manual (2014)
[16] Brown, CE; Urban, J.; Kohlhase, M. (ed.); Johansson, M. (ed.); Miller, BR (ed.); Moura, L. (ed.); Tompa, FW (ed.), Extracting higher-order goals from the Mizar Mathematical Library, 99-114, (2016), Berlin · Zbl 1344.68203
[17] Byliński, C., Introduction to categories and functors, Formaliz. Math., 1, 409-420, (1990)
[18] Corbineau, P.; Miculan, M. (ed.); Scagnetto, I. (ed.); Honsell, F. (ed.), A declarative language for the Coq proof assistant, 69-84, (2007), Berlin
[19] Dahn, I.; Caferra, R. (ed.); Salzer, G. (ed.), Interpretation of a Mizar-like logic in first-order logic, 137-151, (1998), Berlin
[20] Dahn, I., Wernhard, C.: First order proof problems extracted from an article in the Mizar Mathematical Library. In: Bonacina, M.P., Furbach, U. (eds.) First-Order Theorem Proving (FTP 1997), RISC-Linz Report Series No. 97-50, pp. 58-62. Johannes Kepler Universität, Linz (1997)
[21] Davis, M.; Hayes, PJ (ed.), Obvious logical inferences, 530-531, (1981), Burlington
[22] Moura, LM; Kong, S.; Avigad, J.; Doorn, F.; Raumer, J.; Felty, AP (ed.); Middeldorp, A. (ed.), The Lean theorem prover (system description), 378-388, (2015), Berlin · Zbl 1465.68279
[23] Dunchev, C.; Coen, CS; Tassi, E.; Dowek, G. (ed.); Licata, DR (ed.); Alves, S. (ed.), Implementing HOL in an higher order logic programming language, 4:1-4:10, (2016), Albion
[24] Elgot, CC; Robinson, A., Random-access stored-program machines, an approach to programming languages, J. ACM, 11, 365-399, (1964) · Zbl 0192.07302
[25] Felty, AP; Gunter, EL; Hannan, J.; Miller, D.; Nadathur, G.; Scedrov, A.; Lusk, EL (ed.); Overbeek, RA (ed.), Lambda-Prolog: an extended logic programming language, 754-755, (1988), Berlin
[26] Fitch, F.B.: Symbolic Logic. An Introduction. The Ronald Press Company, New York (1952) · Zbl 0049.00504
[27] Grabowski, A.; Korniłowicz, A.; Naumowicz, A., Mizar in a nutshell, J. Formaliz. Reason., 3, 153-245, (2010) · Zbl 1211.68369
[28] Grabowski, A.; Korniłowicz, A.; Naumowicz, A., Four decades of Mizar, J. Autom. Reason., 55, 191-198, (2015) · Zbl 1336.00111
[29] Hähnle, R., Kerber, M., Weidenbach, C.: Common syntax of the DFGSchwerpunktprogramm deduction. Technical Report TR 10/96, Fakultät für Informatik, Universität Karlsruhe, Karlsruhe, Germany (1996)
[30] Harrison, J.; Wright, J. (ed.); Grundy, J. (ed.); Harrison, J. (ed.), A Mizar mode for HOL, 203-220, (1996), Berlin
[31] Hilbert, D.: Foundations of Geometry. Open Court, Illinois (1971) · Zbl 0228.50002
[32] 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
[33] Jaśkowski, S., On the rules of suppositions, Studia Logica, 1, 32, (1934) · Zbl 0011.09702
[34] Kaliszyk, C.; Pąk, K.; Blamer, J. (ed.); Kutsia, T. (ed.); Simos, D. (ed.), Isabelle formalization of set theoretic structures and set comprehensions, (2017), Berlin · Zbl 07036050
[35] Kaliszyk, C.; Pąk, K.; Geuvers, H. (ed.); England, M. (ed.); Hasan, O. (ed.); Rabe, F. (ed.); Teschke, O. (ed.), Presentation and manipulation of Mizar properties in an Isabelle object logic, 193-207, (2017), Berlin · Zbl 1367.68250
[36] Kaliszyk, C., Pąk, K.: Progress in the independent certification of Mizar Mathematical Library in Isabelle. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Proceedings of the 2017 Federated Conference on Computer Science and Information Systems, FedCSIS 2017, pp. 227-236 (2017)
[37] Kaliszyk, C., Pąk, K., Urban, J.: Towards a Mizar environment for Isabelle: Foundations and language. In: Avigad, J., Chlipala, A. (eds.) Proceedings of 5th Conference on Certified Programs and Proofs (CPP 2016), pp. 58-65. ACM (2016)
[38] Kaliszyk, C.; Urban, J., MizAR 40 for Mizar 40, J. Autom. Reason., 55, 245-256, (2015) · Zbl 1356.68191
[39] Kaliszyk, C., Wiedijk, F.: Merging procedural and declarative proof. In: Berardi, S., Damiani, F., de’Liguoro, U. (eds.) Types for Proofs and Programs, International Conference, TYPES 2008, Volume 5497 of LNCS, pp. 203-219. Springer, Berlin (2008) · Zbl 1246.68198
[40] Kobayashi, N. (ed.): Proceedings Eighth Workshop on Intersection Types and Related Systems, ITRS 2016, Volume 242 of EPTCS (2017)
[41] Korniłowicz, A., Flexary connectives in Mizar, Comput. Lang. Syst. Struct., 44, 238-250, (2015) · Zbl 1387.68207
[42] Korniłowicz, A.; Schwarzweller, C., Computers and algorithms in Mizar, Mech. Math. Appl., 4, 43-50, (2005)
[43] Krauss, A.; Schropp, A.; Kaufmann, M. (ed.); Paulson, LC (ed.), A mechanized translation from higher-order logic to set theory, 323-338, (2010), Berlin · Zbl 1291.68355
[44] Kuncar, O., Popescu, A.: A consistent foundation for Isabelle/HOL. In: Urban, C., Zhang, X. (eds.) Interactive Theorem Proving - 6th International Conference, ITP 2015, Volume 9236 of LNCS, pp. 234-252. Springer, Berlin (2015) · Zbl 1433.68556
[45] Kuncar, O.; Popescu, A., Safety and conservativity of definitions in HOL and Isabelle/HOL, PACMPL, 2, 24:1-24:26, (2018)
[46] Kunčar, O.: Reconstruction of the Mizar type system in the HOL light system. In: Pavlu, J., Safrankova, J. (eds.) WDS Proceedings of Contributed Papers: Part I—Mathematics and Computer Sciences, pp. 7-12. Matfyzpress (2010)
[47] Lee, G., Rudnicki, P.: Alternative aggregates in Mizar. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Proceedings of 6th International Conference on Mathematical Knowledge Management (MKM 2007), Volume 4573 of LNCS, pp. 327-341. Springer (2007) · Zbl 1202.68385
[48] Megill, N.D.: Metamath: A Computer Language for Pure Mathematics. Lulu Press, Morrisville (2007)
[49] Merz, S.; Rodošek, R. (ed.), Mechanizing TLA in Isabelle, 54-74, (1995), Maribor
[50] Nakamura, Y.; Trybulec, A., A mathematical model of CPU, Formaliz. Math., 3, 151-160, (1992)
[51] Naraschewski, W., Wenzel, M.: Object-oriented verification based on record subtyping in higher-order logic. In: Grundy, J., Newey, M.C. (eds) Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs’98, volume 1479 of LNCS, pp. 349-366. Springer, Berlin (1998) · Zbl 0927.03026
[52] Naumowicz, A.; Grabowski, A. (ed.); Naumowicz, A. (ed.), Enhanced processing of adjectives in Mizar, 89-101, (2009), Białystok
[53] 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
[54] Naumowicz, A., Byliński, C.: Improving Mizar texts with properties and requirements. In: Asperti et al. [5], pp. 290-301 · Zbl 1108.68598
[55] Naumowicz, A.; Korniłowicz, A.; Berghofer, S. (ed.); Nipkow, T. (ed.); Urban, C. (ed.); Wenzel, M. (ed.), A brief overview of Mizar, 67-72, (2009), Berlin · Zbl 1252.68262
[56] Naumowicz, A.; Piliszek, R.; Kohlhase, M. (ed.); Johansson, M. (ed.); Miller, BR (ed.); Moura, L. (ed.); Tompa, FW (ed.), Accessing the Mizar library with a weakly strict Mizar parser, 77-82, (2016), Berlin · Zbl 1344.68211
[57] Obua, S.; Barkaoui, K. (ed.); Cavalcanti, A. (ed.); Cerone, A. (ed.), Partizan games in Isabelle/HOLZF, 272-286, (2006), Berlin · Zbl 1168.68543
[58] Obua, S., Fleuriot, J.D., Scott, P., Aspinall, D.: ProofPeer: collaborative theorem proving. CoRR. arXiv:1404.6186 (2014)
[59] Obua, S., Fleuriot, J.D., Scott, P., Aspinall, D.: Type Inference for ZFH. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) Intelligent Computer Mathematics—International Conference, CICM, Volume 9150 of LNCS, pp. 87-101. Springer (2015) · Zbl 1417.68191
[60] Ono, K., On a practical way of describing formal deductions, Nagoya Math. J., 21, 115-121, (1962) · Zbl 0111.00703
[61] Paulson, L.C.: Isabelle: the next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and Computer Science (1990), pp. 361-386 (1990)
[62] Paulson, LC, Set theory for verification: I. From foundations to functions, J. Autom. Reason., 11, 353-389, (1993) · Zbl 0802.68128
[63] Pąk, K., Topological manifolds, Formaliz. Math., 22, 179-186, (2014) · Zbl 1352.57030
[64] Rabe, F., A logical framework combining model and proof theory, Math. Struct. Comput. Sci., 23, 945-1001, (2013) · Zbl 1326.03082
[65] Rudnicki, P., Obvious inferences, J. Autom. Reason., 3, 383-393, (1987) · Zbl 0641.68141
[66] Schürmann, C.: The Twelf proof assistant. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Volume 5674 of LNCS, pp. 79-83. Springer, Berlin (2009) · Zbl 1252.68263
[67] Syme, D.; Bertot, Y. (ed.); Dowek, G. (ed.); Hirschowitz, A. (ed.); Paulin-Mohring, C. (ed.); Théry, L. (ed.), Three tactic theorem proving, 203-220, (1999), Berlin · Zbl 0944.68162
[68] Trybulec, A.; Korniłowicz, A.; Naumowicz, A.; Kuperberg, KT, Formal mathematics for mathematicians—special issue, J. Autom. Reason., 50, 119-121, (2013)
[69] Urban, J., MPTP—motivation, implementation, first experiments, J. Autom. Reason., 33, 319-339, (2004) · Zbl 1075.68081
[70] Urban, J.; Kohlhase, M. (ed.), XML-izing Mizar: making semantic processing and presentation of MML easy, 346-360, (2005), Berlin · Zbl 1151.68681
[71] Urban, J., MizarMode—an integrated proof assistance tool for the Mizar way of formalizing mathematics, J. Appl. Logic, 4, 414-427, (2006) · Zbl 1107.68103
[72] Urban, J., MoMM—fast interreduction and retrieval in large libraries of formalized mathematics, Int. J. Artif. Intell. Tools, 15, 109-130, (2006)
[73] Urban, J., MPTP 0.2: design, implementation, and initial experiments, J. Autom. Reason., 37, 21-43, (2006) · Zbl 1113.68095
[74] Urban, J.; Bancerek, G., Presenting and explaining Mizar, Electr. Notes Theor. Comput. Sci., 174, 63-74, (2007) · Zbl 1278.68283
[75] Urban, J.; Hoder, K.; Voronkov, A.; Fukuda, K. (ed.); Hoeven, J. (ed.); Joswig, M. (ed.); Takayama, N. (ed.), Evaluation of automated theorem proving on the Mizar Mathematical Library, 155-166, (2010), Berlin · Zbl 1294.68128
[76] Urban, J.; Rudnicki, P.; Sutcliffe, G., ATP and presentation service for Mizar formalizations, J. Autom. Reason., 50, 229-241, (2013) · Zbl 1260.68380
[77] 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
[78] Weidenbach, C., Afshordel, B., Brahm, U., Cohrs, C., Engel, T., Keen, E., Theobalt, C., Topić, D.: System description: SPASS version 1.0.0. In: Automated Deduction - CADE-16, volume 1632 of LNCS, pp. 378-382. Springer (1999). https://doi.org/10.1007/3-540-48660-7_34
[79] Wenzel, M.: Isar—a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs 1999, Volume 1690 of LNCS, pp. 167-184. Springer (1999)
[80] Wenzel, M.; Klein, G. (ed.); Gamboa, R. (ed.), Asynchronous user interaction and tool integration in Isabelle/PIDE, 515-530, (2014), Berlin · Zbl 1416.68182
[81] Wenzel, M.: The Isabelle/Isar reference manual (2017)
[82] Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle framework. In: Mohamed, O.A., Muñoz, C.A., Tahar, S. (eds.) Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Volume 5170 of LNCS, pp. 33-38. Springer (2008) · Zbl 1165.68478
[83] Wenzel, M.; Wiedijk, F., A comparison of Mizar and Isar, J. Autom. Reason., 29, 389-411, (2002) · Zbl 1064.68083
[84] Wiedijk, F.: CHECKER—notes on the basic inference step in Mizar. http://www.cs.kun.nl/ freek/mizar/by.dvi (2000). Accessed 25 Aug 2018
[85] Wiedijk, F.; Boulton, RJ (ed.); Jackson, PB (ed.), Mizar light for HOL light, 378-394, (2001), Berlin · Zbl 1005.68539
[86] Wiedijk, F.: A synthesis of the procedural and declarative styles of interactive theorem proving. Log. Methods Comput. Sci. 8(1:30), 1-26 (2012) · Zbl 1238.68147
[87] Zhan, B.; Ayala-Rincón, M. (ed.); Muñoz, CA (ed.), Formalization of the fundamental group in untyped set theory using auto2, 514-530, (2017), Berlin · Zbl 1468.68331
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.