Version 7.9.03

[Adam Naumowicz]

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. [phone]
Institute of Computer Science          tel. [phone] (office)
University of Bialystok                e-mail: adamn@...
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================