[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: RELITERS

On Thu, Jan 18, 2001 at 03:14:44PM +0100, Artur Kornilowicz wrote:

> I have checked how many errors RELITERS enhancer reports in Mizar
> Mathematical Library. RELITERS finds out superfluous steps in iterative
> equalities. It only reports errors, does not remove.
> 
> The results are as follows:
> 
>            NAME   COUNT
> 
>     1  ASYMPT_1   479
>     2     INT_3   370
>     3  SCMBSORT   363
>     4   SIN_COS   326
>     5  QUOFIELD   285
>     6  SCMISORT   277
>     7     GCD_1   268

>     .........

It is not a surprise to me that ASYMPT_1 has taken the first place
in this ranking.  This article contains a solution to quite a numer
of exercises from a book about asymptotic notation and it was written
by two students under my supervision.  They were learning Mizar at
that time and they were doing reasoning steps that they could follow
without paying much attention to the checker abilities.

It only indicates that a utility which actually removes superflous 
steps in iterative equalities is needed.

Cheers,

Piotr Rudnicki               CompSci, Univerity of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca                 http://web.cs.ualberta.ca/~piotr