Abstract
In this paper, we present a remote verification environment for Mizar and its integration with a web platform. Although a VSCode extension for Mizar is already available, it requires installing the Mizar verification tools locally. Our newly developed system implements these verification environments on a server, eliminating this requirement. First, we explain the implementation of the remote verification environment for Mizar and the VSCode for the Web extension. Second, we discuss the integration with the web platform emwiki, which allows browsing the existing Mizar Mathematical Library (MML).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
- 3.
- 4.
- 5.
- 6.
- 7.
- 8.
- 9.
- 10.
References
Taniguchi, H., Nakasho, K.: Visual studio code extension and auto-completion for Mizar language. In: 2021 Ninth International Symposium on Computing and Networking (CANDAR), pp. 182–188. IEEE (2021)
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). https://doi.org/10.1007/978-3-540-27818-4_4
Grabowski, A., Kornilowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formalized Reasoning 3(2), 153–245 (2010)
Bancerek, G., et al.: Mizar: state-of-the-art and beyond. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 261–279. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-20615-8_17
Arias, E.J.G., Pin, B., Jouvelot, P.: jsCoq: towards hybrid theorem proving interfaces. arXiv preprint arXiv:1701.07125 (2017)
Wenzel, M.: Isabelle/PIDE after 10 years of development. In: 13th International Workshop on User Interfaces for Theorem Provers (UITP 2018), Oxford, UK (2018)
Lüth, C., Ring, M.: A web interface for Isabelle: the next generation. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 326–329. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39320-4_22
Ring, M., Lüth, C.: Collaborative interactive theorem proving with clide. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 467–482. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08970-6_30
Xu, H., Zhao, Y.: Isabelle/cloud: delivering Isabelle/HOL as a cloud IDE for theorem proving. In: Proceedings of the 14th Asia-Pacific Symposium on Internetware, pp. 313–322 (2023)
Kaliszyk, C., Urban, J.: Mizar 40 for Mizar 40. J. Autom. Reason. 55(3), 245–256 (2015)
Jakubŭv, J.,et al.: Mizar 60 for Mizar 50. arXiv preprint arXiv:2303.06686 (2023)
Yamamichi, D., Shigenaka, S., Nakasho, K., Wasaki, K.: A web platform for hosting the Mizar mathematical library (2022)
Furushima, H., Yamamichi, D., Shigenaka, S., Nakasho, K., Wasaki, K.: An integrated web platform for the Mizar mathematical library. In: Buzzard, K., Kutsia, T. (eds.) CICM 2022. LNCS, vol. 13467, pp. 141–146. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-16681-5_9
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.) CICM 2011. LNCS (LNAI), vol. 6824, pp. 133–148. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22673-1_10
Tankink, C., Kaliszyk, C., Urban, J., Geuvers, H.: Formal mathematics on display: a wiki for flyspeck. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 152–167. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39320-4_10
Nakasho, K., Shidama, Y.: Documentation generator focusing on symbols for the HTML-ized Mizar library. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 343–347. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-20615-8_25
Shigenaka, S.: Research on quality measurement of the Mizar mathematical library using dependency graph (2022)
Suzuki, S., Nagasaki, M., Nakasho, K.: Classification and dependency visualization of the articles of the Mizar mathematical library. In: MathUI 2023: 14th Workshop on Mathematical User Interaction, 04–08 September 2023, Cambridge, UK (2023)
Miyata, H., Matsumoto, R., Nakasho, K.: VSCode extension for the web and coding assistance for the Mizar language. In: MathUI 2023: 14th Workshop on Mathematical User Interaction, 04–08 September 2023, Cambridge, UK (2023)
Acknowledgments
This work was supported by JSPS KAKENHI Grant Number 24K14897.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Kai, T., Teruya, Y., Nakasho, K. (2024). Remote Verification System for Mizar Integrated with Emwiki. In: Kohlhase, A., Kovács, L. (eds) Intelligent Computer Mathematics. CICM 2024. Lecture Notes in Computer Science(), vol 14960. Springer, Cham. https://doi.org/10.1007/978-3-031-66997-2_19
Download citation
DOI: https://doi.org/10.1007/978-3-031-66997-2_19
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-66996-5
Online ISBN: 978-3-031-66997-2
eBook Packages: Computer ScienceComputer Science (R0)