Annals of Computer Science and Information Systems, Volume 18

DOI: http://dx.doi.org/10.15439/2019F151

Citation: Proceedings of the 2019 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 18, pages 77–80 (2019)

Full text

Abstract. In this paper, we explain the development of a new Mizar tokenizer and parser program as a component of a search system that works on the Mizar Mathematical Library. The existing Mizar tokenizer and parser can handle only an article as a whole written in the Mizar language, however, the newly developed program can deal with a snippet of a Mizar article. In particular, since it is possible to handle a snippet of an article without specifying a vocabulary section of an environment part, it is expected that user input efforts will be greatly reduced.

References

1. G. Bancerek, C. Byliński, A. Grabowski, A. Korniłowicz, R. Matuszewski, A. Naumowicz, and K. Pąk, “The role of the Mizar Mathematical Library for interactive proof development in Mizar,” Journal of Automated Reasoning, vol. 61, no. 1, pp. 9–32, Jun 2018. [Online]. Available: https://doi.org/10.1007/s10817-017-9440-6
2. G. Bancerek, “Information retrieval and rendering with MML query,” in Mathematical Knowledge Management, J. M. Borwein and W. M. Farmer, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2006, pp. 266–279. [Online]. Available: https://doi.org/10.1007/11812289_21
3. F. Guidi and C. Sacerdoti Coen, “A survey on retrieval of mathematical knowledge,” Mathematics in Computer Science, vol. 10, no. 4, pp. 409–427, Dec 2016. [Online]. Available: https://doi.org/10.1007/s11786-016-0274-0
4. C. Bylinski and J. Alama, “New developments in parsing Mizar,” in Intelligent Computer Mathematics, J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012, pp. 427–431. [Online]. Available: https://doi.org/10.1007/978-3-642-31374-5_30
5. A. Naumowicz and R. Piliszek, “Accessing the Mizar library with a weakly strict Mizar parser,” in Intelligent Computer Mathematics, M. Kohlhase, M. Johansson, B. Miller, L. de Moura, and F. Tompa, Eds. Cham: Springer International Publishing, 2016, pp. 77–82. [Online]. Available: https://doi.org/10.1007/978-3-319-42547-4_6
6. P. Cairns and J. Gow, “Integrating searching and authoring in Mizar,” Journal of Automated Reasoning, vol. 39, no. 2, pp. 141–160, Aug 2007. [Online]. Available: https://doi.org/10.1007/s10817-007-9073-2
7. A. W. Appel and D. B. MacQueen, “Standard ML of New Jersey,” in International Symposium on Programming Language Implementation and Logic Programming. Springer, 1991, pp. 1–13. [Online]. Available: https://doi.org/10.1007/3-540-54444-5_83
8. C. Kaliszyk, J. Urban, and J. Vyskočil, “Learning to parse on aligned corpora (rough diamond),” in International Conference on Interactive Theorem Proving. Springer, 2015, pp. 227–233. [Online]. Available: https://doi.org/10.1007/978-3-319-22102-1_15