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

Re: [mizar] Mizar 7.8.07 accepts an incorrect inference?

Hi Bill,

On Wed, 26 Dec 2007, Chisolm, Bill wrote:
Am I misunderstanding some fundamental idea here? Could this really be a bug in the Mizar verifier?
It's really a bug in the schematizer - thanks for a nice Christmas present ;-))) It seems that it's been around for two and a half years! I made a quick fix which should correct it and now I'm checking the MML for similar errors as your example - fortunately haven't found any so far ;-) 


theorem Th1:    :: Surely there should be an error here somewhere.
 1 = 0
proof
 assume 1 <> 0;

 B1: 3 = 2 + 1;
 B2: not ex c being Nat st 2 < c & c < 3  from MyScheme(B1);
 B3:     ex c being Nat st 2 < c & c < 3  from MyScheme(B1);


The above line should of course be marked as erroneous.


 thus contradiction by B2, B3;
end;

theorem Th2:    :: This also deserves an error message.
 for c being Nat holds 2 < c & c < 3
proof
 C1: 3 = 2 + 1;
 thus thesis from MyScheme(C1);
end;


Thanks again for your bug report.
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/
======================================================================