[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: RE[mizar] LPREM,RELINFER and *603,*604,*605
On Sun, 30 Dec 2007, rk1 wrote:
RELINFER, however, gives me over 400 errors in my file.
Thanks to your example, now I see what all those errors mean: my style
of proof writing is rather "incremental" and I like to use one fact at a
time to go from one statement to the next. You and RELINFER are telling
me I can condense many of these incremental groups of statements into
single steps.
Do I absolutely have to remove all the RELINFER *604 and *605 errors to
prepare my file for submission to the MML?
As far as I know (and the MML web page says so), the MML submission
procedure requires all such errors be removed. So if you don't want to
risk rejecting your article by a picky reviewer, you'd better get rid of
them before submission.
I removed all the *602 and *603 from RELPREM as I agree those make my
proof clearer, but I think condensing many of my chosen steps as
RELINFER suggests would make my proof harder to read.
I agree, I don't really like doing this bit of cleansing myself ;-)
But what one finds easier to read, others may find boring, so I think it's
better to rely on the checker's notion of obviousness.
And 400 errors is not that bad, after all. Also, removing them by hand can
help you improve your style and then write articles faster knowing better
what inferences Mizar can accept.
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/
======================================================================