[mizar] robustness of the Mizar system

["Robert Milewski" <milewski@math.uwb.edu.pl>]

    Dear All

I would like to report briefly my recent work concerning the robustness of
the Mizar system. My first task was to investigate whether permutations of
references influence accepting inference steps as obvious. To enable such
tests I implemented some utility programs, one of them removing 'then'
references (delinker), another separating library references (separator),
and a tool which permutes such separated references. Obviously, checking of
all possible permutations is not realistic, as the number of references in
one inference reaches 23 (article GENEALG1), so the experiment would take
about 4*10^15 years. Therefore, in my tests the order of references is
generated randomly. This experiment was repeated 10 times and showed that
during processing articles PENCIL_1, YELLOW15, BORSUK_1, and T_1TOPSP
several errors *4 were reported. The bug appeared to concern the so called
"partial building-in of former theorem BOOLE:11" (x in X & X c= Y implies x
in Y). The bug was fixed by Adam Naumowicz in the Mizar version 6.1.14.

My another experiment concerned monotonicity of references. To check this I
wrote a program which to every inference randomly adds one of accessible
local references. This test was also repeated 10 times on the whole Mizar
library which revealed another bug (Mizar reported errors *4 on articles
FUNCTOR3 and TSP_2). The error concerned the radix type rounding-up
algorithm in equalizer, and was fixed in Mizar version 6.1.16.

Third kind of experiments was directed to find and remove repeated steps
within proofs. A utility run on the whole library gave the following
results:
before revision: 51 275 019 bytes
after revision:  51 038 106 bytes
so the difference makes 236 913 bytes (approx. 0.46%).
In the nearest future the results of this revision will be incorporated into
MML. At the moment I'm working on a program which will enable moving some
statements outside the proof blocks if they do not use any local variables.
Then the experiment with the program removing equivalent statements will be
repeated.

    Robert Milewski