Re: [mizar] Re: what's new in mizar?

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

I am not sure if  'quite a few such cases' is correct, I believe that hundreds TRIVDEMO "errors" had been
reported. All are corrected. However, I observed that many of them are not related to the new checker,
because cleaning of MML was neglected. Still, it was a little bit more than 'quite a few'.
The common gain was about 0.1 %  (MML became shorter by 0.1%),
 Adam is right of course that important test is RELINFER.

Czeslaw had implemented a more stronger checker but afterwards we decided that we have to be more
careful. So, new checker allows for one resolution, in a very restricted situation. The most important are quantitative limits:
two clauses, one pair of basic sentences that may be unified.
Of cause the restrictions will be relaxed in the future, the problem is how to do it?

As  yet I would not advise to use the new feature while writing the article. After articler is completed one may use RELINFER and other utilities to remove some lines (probably few of them if any) and to get the article a little more readable.

Regards,
Andrzej

Jesse Alama wrote:

Adam Naumowicz <adamn@math.uwb.edu.pl> writes:

  

Indeed, there were quite a few such cases where 'trivdemo' detected
proofs that could be simplified to a straightforward justification
(see. RELAT_1:9 for example). But adjusting the library according to
what 'relinfer' reports is even more important.
    

Do you have some numbers here?  It would be interesting to know, for
example, how many lines from the MML can now be safely deleted thanks to
the improved checker.

Jesse