[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: RE[mizar] LPREM,RELINFER and *603,*604,*605
Hello,
On Sat, 29 Dec 2007, rk1 wrote:
When I run RELPREM and RELINFER, I get a lot of *603, *604, and *605 errors
in my file, but removing the indicated labels or statements causes my proofs
to break. Is this normal?
It's quite typical that RELPREM and RELIFER report some irrelevant
references or inference steps which may be simplified - the users may
sometimes underestimate the power of Mizar's checker.
But one should be careful when improving their articles to get rid of
RELPREM and RELINFER warnings. There are some basic rules.
Let's take the following proof example:
environ
begin
let a,b,c,d,e be set;
assume A: a = b;
assume B: b = c;
assume C: c = d;
assume D: d = e;
then a = c by A,B;
a = c by A,B,C;
a = c by A,B;
then a = d by C;
E: a = c by A,B;
a = d by C,E;
end;
The text is logically correct (there are no verifier errors), but there
are some irrelevant items. After running RELPREM we get:
now
let a,b,c,d,e be set;
assume A: a = b;
assume B: b = c;
assume C: c = d;
then a = c by A,B;
::> *603
:: Here the 'then' linking is irrelevant
a = c by A,B,C;
::> *602
:: Here referring to the 'C' label is irrelevant
:: so in both cases the statements should be reduced to 'a = c by A,B;'
a = c by A,B;
then a = d by C;
E: a = c by A,B;
a = d by C,E;
a = d by A,B,C;
end;
::> 602: Irrelevant reference
::> 603: Irrelevant linking
Similarly, RELINFER reports the following:
now
let a,b,c,d,e be set;
assume A: a = b;
assume B: b = c;
assume C: c = d;
then a = c by A,B;
a = c by A,B,C;
a = c by A,B;
then a = d by C;
::> *605
:: Here the 'then' linking should be replaced by appending all references
:: used in the previous stetement (somethimes also with 'then')
E: a = c by A,B;
a = d by C,E;
::> *604
:: Here is the case with a reference to a label rather than by 'then'.
:: As above, one should replace 'E' with 'A,B' (the order should not matter).
a = d by A,B,C;
end;
::> 604: Irrelevant inference
::> 605: Irrelevant linked inference
Please note that when many RELINFER errors are reported in consecutive
steps, one should improve them one at a time and check with the verifier
if everything is still correct. And, of course, everything said about
'then' concerns 'hence' as well.
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/
======================================================================