|
Dear Prof. Adam Naumowicz and Prof. Bill Chisolm, Thank you very much for your bug reports and quick response. Now we are preparing the fundamental theorems for formalization proof of Poincare's lemma(by Grisha Perelman ) systematically. Quite a lot of time is necessary for it. So we need the " normal systems" as soon as possible. Best regards, Yasunari Shidama > Date: Thu, 27 Dec 2007 11:32:09 +0100 > From: adamn@math.uwb.edu.pl > To: mizar-forum@mizar.uwb.edu.pl > Subject: 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/ > ===============! ======================================================= > |