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.2023.37
URN: urn:nbn:de:0030-drops-184121
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18412/
Grabowski, Adam ;
Korniłowicz, Artur
Implementing More Explicit Definitional Expansions in Mizar (Short Paper)
Abstract
The Mizar language and its corresponding proof-checker offers the tactic of definitional expansions in proof skeletons. This apparatus is rather fragile in the case of intensive overloading of notions (which is widely observed e.g. in the field of algebra, but it is also present in the more fundamental set-theory contexts). We propose the extension of this mechanism: the change should offer users the more precise control over expansions via choosing the right definitional variant for the proof under consideration, still letting the authors to retain the more conservative approach. As a rule, the change will affect new Mizar texts, but obviously, it allows also for solving some context conflicts caused by the original approach in the Mizar repository. The usefulness of our approach is shown by a number of experiments carried out within MML, which is also affected by the change.
BibTeX - Entry
@InProceedings{grabowski_et_al:LIPIcs.ITP.2023.37,
author = {Grabowski, Adam and Korni{\l}owicz, Artur},
title = {{Implementing More Explicit Definitional Expansions in Mizar}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {37:1--37:8},
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/opus/volltexte/2023/18412},
URN = {urn:nbn:de:0030-drops-184121},
doi = {10.4230/LIPIcs.ITP.2023.37},
annote = {Keywords: Mizar, definitions, proof assistants, mechanization of proof}
}
