Abstract
The Mizar language aims to capture mathematical vernacular by providing a rich language for mathematics. From the perspective of a user, the richness of the language is welcome because it makes writing texts more “natural”. But for the developer, the richness leads to syntactic complexity, such as dealing with overloading.
Recently the Mizar team has been making a fresh approach to the problem of parsing the Mizar language. One aim is to make the language accessible to users and other developers. In this paper we describe these new parsing efforts and some applications thereof, such as large-scale text refactorings, pretty-printing, HTTP parsing services, and normalizations of Mizar texts.
Supported by the ESF research project Dialogical Foundations of Semantics within the ESF Eurocores program LogICCC (funded by the Portuguese Science Foundation, FCT LogICCC/0001/2007). Research for this paper was partially done while a visiting fellow at the Isaac Newton Institute for the Mathematical Sciences in the program ‘Semantics & Syntax’. Karol Pąk deserves thanks for his patient assistance in developing customized Mizar text rewriting tools.
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
Preview
Unable to display preview. Download preview PDF.
References
Aho, A., Lam, M., Sethi, R., Ullman, J.: Compilers: Principles, Techniques, and Tools. Pearson/Addison Wesley (2007)
de Bruijn, N.G.: AUT-SL, a single-line version of Automath. In: Nederpelt, R., Geuvers, J.H., de Vrijer, R.C. (eds.) Selected Papers on Automath. Studies in Logic and the Foundations of Mathematics, vol. 133, ch. B.2, pp. 275–281. North-Holland (1994)
Grabowski, A., Kornilowicz, A., Naumowicz, A.: Mizar in a nutshell. Journal of Formalized Reasoning 3(2), 153–245 (2010)
Matuszewski, R., Rudnicki, P.: Mizar: The first 30 years. Mechanized Mathematics and its Applications 4(1), 3–24 (2005)
Urban, J.: MizarMode—An integrated proof assistance tool for the Mizar way of formalizing mathematics. Journal of Applied Logic 4(4), 414–427 (2006), http://www.sciencedirect.com/science/article/pii/S1570868305000698
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bylinski, C., Alama, J. (2012). New Developments in Parsing Mizar . In: Jeuring, J., et al. Intelligent Computer Mathematics. CICM 2012. Lecture Notes in Computer Science(), vol 7362. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31374-5_30
Download citation
DOI: https://doi.org/10.1007/978-3-642-31374-5_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31373-8
Online ISBN: 978-3-642-31374-5
eBook Packages: Computer ScienceComputer Science (R0)