Development of a flexible Mizar tokenizer and parser for information retrieval system

• Autorzy: Nakasho Kazuhisa

Identyfikatory

DOI

10.15439/2019F151

• Konferencja: Federated Conference on Computer Science and Information Systems (14 ; 01-04.09.2019 ; Leipzig, Germany)
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

formal languages; grammars; information retrieval; mathematics computing; program compilers; software library

PL

języki formalne; gramatyki; wyszukiwanie informacji; obliczenia matematyczne; kompilatory programów; biblioteka oprogramowania

• Wydawca: Polskie Towarzystwo Informatyczne
• Czasopismo: Annals of Computer Science and Information Systems
• Rocznik: 2019
• Tom: Vol. 18
• Strony: 77--80
• Opis fizyczny: Bibliogr. 8 poz., rys., tab.

Twórcy

autor

Nakasho Kazuhisa

• Yamaguchi University in Yamaguchi 2-16-1, Tokiwa-dai, Ube City, Yamaguchi, Japan

Bibliografia

• 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

Uwagi

1. Track 1: Artificial Intelligence and Applications

2. Technical Session: 14th International Symposium Advances in Artificial Intelligence and Applications

3. Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2020).