Definitional Expansions in Mizar
Artur Korniłowicz · Journal of Automated Reasoning · 2015
The Mizar Verifier uses definitional expansions for controlling proof structures. In this paper we propose another use of definitional expansions—enriching verified inferences by expansions of definitions of formulae included in the inferences and increasing the number of premises accessible by Checker. This introduces more knowledge to the reasoning, which helps to draw more conclusions. Some statistics about influence of such expansions on the Mizar Mathematical Library are presented.