2026-07-24T05:47:09Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18412 2024-03-06T11:01:50Z ddc:004 open_access

Implementing More Explicit Definitional Expansions in Mizar (Short Paper) Grabowski, Adam Korniłowicz, Artur Mizar definitions proof assistants mechanization of proof 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Adam Grabowski and Artur Korniłowicz 2023 Is Part Of LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2023.37 urn:nbn:de:0030-drops-184121 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.37 eng https://creativecommons.org/licenses/by/4.0/legalcode