[mizar] Version 7.9.03

[Adam Naumowicz <adamn@math.uwb.edu.pl>]

Dear All,

A new version of the Mizar system (7.9.03) has been released for download. 
The most important change in this version of the verifier is the new 
extension of attribute handling in the equalizer. With this new mechanism, 
the verifier is able to collect ("round-up") all adjectives being 
consequences of conditional and functorial (term) registrations for a 
whole class of equated terms. In practice, some reasonings can now be 
expressed in a more natural way (e.g. with attributive premises) 
eliminating many 'reconsider' statements. Below are two typical examples.

With this conditional registration from RAT_1:

registration
    cluster integer -> rational number;
end;

the old verifier would report:

now
   let a be integer number;
   a is rational;

   let b be number;
   b is integer implies b is rational;
::>                               *4
end;

The second inference is now obvious in 7.9.03. Similarly, in view of
this registration from XXREAL_0:

registration
   cluster non negative non zero -> positive (ext-real number);
end;

the inference below can now be accepted thanks to rounding-up
all attribute consequences in equality classes:

now
   let a,b be real number;
   a is non negative & b is non zero & a=b implies a is positive;
::>                                                          *4
end;

The new version applied to the previous official MML (4.103.1019) reported 
about 8500 unnecessary premises (relprem) and about 600 proofs that may be 
reduced to a straightforward (single "by") justification (trivdemo). When 
removed automatically, it reduced the size of MML by about 250 kB (which 
is more than the size of three average articles).

Please apply the standard utilities on the articles you're currently 
working on to see what unnecessary items they might report. As usual with 
major changes to the verifier, please report any bugs or unexpected 
behavior you encounter with this new version.

Thanks to Josef Urban and Jesse Alama this version has also been released
for two additional OS's: Linux/ARM and Darwin/i386
(downloadable at ftp://mizar.uwb.edu.pl/pub/system/current/ ).

Best regards,
Adam Naumowicz

======================================================================
Department of Applied Logic            fax. +48 (85) 745-7662
Institute of Computer Science          tel. +48 (85) 745-7559 (office)
University of Bialystok                e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================