Hi, On Sun, 30 Dec 2007, Adam Naumowicz wrote:
On Sun, 30 Dec 2007, rk1 wrote: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 don't think that requiring no RELINFER errors in submissions is a perfect policy.
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.
Checker's "notion of obvouisness" can be quite "suboptimal" - try to understand this: http://lipa.ms.mff.cuni.cz/~urban/mmlcpd/mmlcpd.4.87.985/mml/filter_2.miz.html#1592 (no automated theorem prover can reprove that without splitting the conjunction, and manually pruning the premises that are irrelevant for each conjunct).
I think that what checker accepts should be used as an (always imperfect) "obviousness upper bound", and not be forced on authors and readers also as a lower bound by requiring no RELINFER errors. These errors should be used as suggestions (especially as Adam says, to learn occasionally that checker can newly handle something obvious), which can be rejected by the author.
Best, Josef