License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2021.11
URN: urn:nbn:de:0030-drops-139064
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13906/
Go to the corresponding LIPIcs Volume Portal

Byliński, Czesław ; Korniłowicz, Artur ; Naumowicz, Adam

Syntactic-Semantic Form of Mizar Articles

pdf-format:
LIPIcs-ITP-2021-11.pdf (0.7 MB)

Abstract

Mizar Mathematical Library is most appreciated for the wealth of mathematical knowledge it contains. However, accessing this publicly available huge corpus of formalized data is not straightforward due to the complexity of the underlying Mizar language, which has been designed to resemble informal mathematical papers. For this reason, most systems exploring the library are based on an internal XML representation format used by semantic modules of Mizar. This representation is easily accessible, but it lacks certain syntactic information available only in the original human-readable Mizar source files. In this paper we propose a new XML-based format which combines both syntactic and semantic data. It is intended to facilitate various applications of the Mizar library requiring fullest possible information to be retrieved from the formalization files.

BibTeX - Entry

@InProceedings{bylinski_et_al:LIPIcs.ITP.2021.11,
  author =	{Byli\'{n}ski, Czes{\l}aw and Korni{\l}owicz, Artur and Naumowicz, Adam},
  title =	{{Syntactic-Semantic Form of Mizar Articles}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{11:1--11:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/13906},
  URN =		{urn:nbn:de:0030-drops-139064},
  doi =		{10.4230/LIPIcs.ITP.2021.11},
  annote =	{Keywords: Mizar system, mathematical knowledge representation, XML representation}
}

Keywords: Mizar system, mathematical knowledge representation, XML representation
Collection: 12th International Conference on Interactive Theorem Proving (ITP 2021)
Issue Date: 2021
Date of publication: 21.06.2021
Supplementary Material: A collection of prototype hyper-linked Mizar articles generated from the new ESM syntactic-semantic format can be found at
Dataset: http://alioth.uwb.edu.pl/~artur/mmlesx/

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI