An integrated web platform for the Mizar Mathematical Library. (English) Zbl 07691295
Buzzard, Kevin (ed.) et al., Intelligent computer mathematics. 15th international conference, CICM 2022, Tbilisi, Georgia, September 19–23, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13467, 141-146 (2022).
Summary: This paper reports on the development of a Web platform to host the Mizar Mathematical Library (MML). In recent years, the size of formalized mathematical libraries has been drastically increasing, and this has led to a growing demand for tools that support efficient and comprehensive browsing, searching, and annotation of these libraries. This platform implements a Wiki function to add comments to the HTMLized MML, three types of search function (article, symbol, and theorem), and a function to show the dependency graph of the MML. This platform is designed with consistency, scalability, and interoperability as top priorities for long-term use.
For the entire collection see [Zbl 1511.68013].
For the entire collection see [Zbl 1511.68013].
MSC:
| 68Vxx | Computer science support for mathematical research and practice |
References:
| [1] | Alama, J.; Davenport, JH; Farmer, WM; Urban, J.; Rabe, F., mizar-items: exploring fine-grained dependencies in the Mizar mathematical library, Intelligent Computer Mathematics, 276-277 (2011), Heidelberg: Springer, Heidelberg · Zbl 1335.68255 · doi:10.1007/978-3-642-22673-1_19 |
| [2] | Alama, J.; Brink, K.; Mamane, L.; Urban, J.; Davenport, JH; Farmer, WM; Urban, J.; Rabe, F., Large formal wikis: issues and solutions, Intelligent Computer Mathematics, 133-148 (2011), Heidelberg: Springer, Heidelberg · Zbl 1335.68220 · doi:10.1007/978-3-642-22673-1_10 |
| [3] | Alama, J.; Mamane, L.; Urban, J.; Jeuring, J., Dependencies in formal mathematics: applications and extraction for coq and Mizar, Intelligent Computer Mathematics, 1-16 (2012), Heidelberg: Springer, Heidelberg · Zbl 1335.68221 · doi:10.1007/978-3-642-31374-5_1 |
| [4] | Bancerek, G., The role of the Mizar mathematical library for interactive proof development in Mizar, J. Autom. Reasoning, 61, 1, 9-32 (2018) · Zbl 1433.68530 · doi:10.1007/s10817-017-9440-6 |
| [5] | Bancerek, G.; Rudnicki, P.; Asperti, A.; Buchberger, B.; Davenport, JH, Information retrieval in MML, Mathematical Knowledge Management, 119-132 (2003), Heidelberg: Springer, Heidelberg · Zbl 1022.68610 · doi:10.1007/3-540-36469-2_10 |
| [6] | Cairns, P.; Gow, J., Integrating searching and authoring in Mizar, J. Autom. Reasoning, 39, 2, 141-160 (2007) · Zbl 1129.68500 · doi:10.1007/s10817-007-9073-2 |
| [7] | Cervone, D., MathJax: a platform for mathematics on the Web, Not. AMS, 59, 2, 312-316 (2012) · Zbl 1237.68242 |
| [8] | van Doorn, F.; Ebner, G.; Lewis, RY; Benzmüller, C.; Miller, B., Maintaining a library of formal mathematics, Intelligent Computer Mathematics, 251-267 (2020), Cham: Springer, Cham · Zbl 1455.68262 · doi:10.1007/978-3-030-53518-6_16 |
| [9] | Grabowski, A.; Korniłowicz, A.; Naumowicz, A., Four decades of Mizar, J. Autom. Reasoning, 55, 3, 191-198 (2015) · Zbl 1336.00111 · doi:10.1007/s10817-015-9345-1 |
| [10] | Heras, J., Komendantskaya, E.: HoTT formalisation in coq: dependency graphs & ML4PG. arXiv preprint arXiv:1403.2531 (2014) |
| [11] | Marcus, R.; Kohlhase, M.; Rabe, F.; Benzmüller, C.; Miller, B., TGView3D: a system for 3-dimensional visualization of theory graphs, Intelligent Computer Mathematics, 290-296 (2020), Cham: Springer, Cham · Zbl 1455.68267 · doi:10.1007/978-3-030-53518-6_20 |
| [12] | Matuszewski, R.; Rudnicki, P., Mizar: the first 30 years, Mechanized Math. Appl., 4, 1, 3-24 (2005) |
| [13] | Nakasho, K.; Shidama, Y.; Kerber, M.; Carette, J.; Kaliszyk, C.; Rabe, F.; Sorge, V., Documentation generator focusing on symbols for the HTML-ized Mizar library, Intelligent Computer Mathematics, 343-347 (2015), Cham: Springer, Cham · Zbl 1417.68212 · doi:10.1007/978-3-319-20615-8_25 |
| [14] | Naumowicz, A.; Kerber, M.; Carette, J.; Kaliszyk, C.; Rabe, F.; Sorge, V., Tools for MML environment analysis, Intelligent Computer Mathematics, 348-352 (2015), Cham: Springer, Cham · Zbl 1417.68213 · doi:10.1007/978-3-319-20615-8_26 |
| [15] | Rudnicki, P.; Trybulec, A.; Asperti, A.; Buchberger, B.; Davenport, JH, On the integrity of a repository of formalized mathematics, Mathematical Knowledge Management, 162-174 (2003), Heidelberg: Springer, Heidelberg · Zbl 0982.68136 · doi:10.1007/3-540-36469-2_13 |
| [16] | Tankink, C.; Kaliszyk, C.; Urban, J.; Geuvers, H.; Carette, J.; Aspinall, D.; Lange, C.; Sojka, P.; Windsteiger, W., Formal mathematics on display: a wiki for flyspeck, Intelligent Computer Mathematics, 152-167 (2013), Heidelberg: Springer, Heidelberg · Zbl 1390.68751 · doi:10.1007/978-3-642-39320-4_10 |
| [17] | Urban, J.; Alama, J.; Rudnicki, P.; Geuvers, H.; Autexier, S., A wiki for Mizar: motivation, considerations, and initial prototype, Intelligent Computer Mathematics, 455-469 (2010), Heidelberg: Springer, Heidelberg · Zbl 1286.68434 · doi:10.1007/978-3-642-14128-7_38 |
| [18] | Urban, J.; Rudnicki, P.; Sutcliffe, G., ATP and presentation service for Mizar formalizations, J. Autom. Reasoning, 50, 2, 229-241 (2013) · Zbl 1260.68380 · doi:10.1007/s10817-012-9269-y |
| [19] | Vyskocil, J., Urban, J.: Disambiguating ProofWiki into Mizar: First steps. AITP 2018 (2018) |
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.
