Search Results

Documents authored by Naumowicz, Adam

Document
Complete Volume
DOI: 10.4230/LIPIcs.ITP.2023
LIPIcs, Volume 268, ITP 2023, Complete Volume

Authors: Adam Naumowicz and René Thiemann

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
LIPIcs, Volume 268, ITP 2023, Complete Volume
Cite as

14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 1-660, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Proceedings{naumowicz_et_al:LIPIcs.ITP.2023,
  title =	{{LIPIcs, Volume 268, ITP 2023, Complete Volume}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{1--660},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023},
  URN =		{urn:nbn:de:0030-drops-183747},
  doi =		{10.4230/LIPIcs.ITP.2023},
  annote =	{Keywords: LIPIcs, Volume 268, ITP 2023, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.ITP.2023.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Adam Naumowicz and René Thiemann

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{naumowicz_et_al:LIPIcs.ITP.2023.0,
  author =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{0:i--0:x},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.0},
  URN =		{urn:nbn:de:0030-drops-183755},
  doi =		{10.4230/LIPIcs.ITP.2023.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.ITP.2021.11
Syntactic-Semantic Form of Mizar Articles

Authors: Czesław Byliński, Artur Korniłowicz, and Adam Naumowicz

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

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.
Cite as

Czesław Byliński, Artur Korniłowicz, and Adam Naumowicz. Syntactic-Semantic Form of Mizar Articles. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 11:1-11:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.ITP.2021.11},
  URN =		{urn:nbn:de:0030-drops-139064},
  doi =		{10.4230/LIPIcs.ITP.2021.11},
  annote =	{Keywords: Mizar system, mathematical knowledge representation, XML representation}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact