Re: RE[mizar] LPREM,RELINFER and *603,*604,*605

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

Josef Urban wrote:

> 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).


If you mean this

A6:  p"\/"(c"/\"a) = (p"\/"c)"/\"a & (p"\/"c)"/\"a"/\"q = a"/\"d & 
a"/\"d = a'
"/\"d'
    by A2,A5,Th74,LATTICES:def 7,def 12;

it is definitely not a good Mizar style. It should be rather

A6: (p"\/"(a"/\"c))"/\"q = (p"\/"c)"/\"a"/\"q by A2,A5,LATTICES:def 12
              .= a"/\"d by LATTICES:def 7
              .= a'"/\"d' by Th74;

I doubt, if we can implement a checker that press the Authors to write 
articles in a good style. And I do not think that
it would be reasonable.

As  RELINFER goes, the rule is that you may leave some RELINFER 
"errors", but you must justify it. The removing error reported by 
RELPREM may cause a combinatorial explosion, the time of processing of 
article jumps up by an order or more. And it is related
to one or two infrences, as a rule. So for one inference it is much worse.

If it is the case then leaving this error is justified, of course.

We want the Authors to correct these errors by hand, because we hope 
that they find out how to do it better. There are tools
that remove errors reported by RELPREM  and RELINFER automatically. It 
the Author mimicks them the quality of the article
gets lower, sometimes.

Regards,
Andrzej