[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] what's new in mizar?
Hi Jesse,
On Wed, 12 Dec 2007, Jesse Alama wrote:
It looks like there's been a new release of mizar (version 7.8.07, MML
4.93.997). What are the new features?
Curious,
The most important change within the system is strengthening the checker
by utilizing two general premises in one disjunct of an inference if they
have a common substitution - "the Scordev device" in the Mizar jargon -
the thing has been discussed for many years, but only now did Andrzej and
Czeslaw agree on a reasonable algorithm and Czeslaw has implemented it,
eventually.
Please search the Mizar-Forum archives for some discussions on this topic:
http://mizar.uwb.edu.pl/cgi-bin/wilma/wilma_glimpse/mizar-forum?query=skordev&Search=Search&errors=0&maxfiles=50&maxlines=10&.cgifields=restricttofiles&.cgifields=case&.cgifields=filelist&.cgifields=lineonly&.cgifields=partial
Practically, with Mizar 7.8.07 you get accepted inferences like the
last one in the text below (not obvious for the 7.8.06 checker):
environ
vocabularies TESTER;
begin
definition
let x be set;
pred P x means contradiction;
pred Q x means contradiction;
pred R x means contradiction;
end;
a: for x being set st P x holds Q x @proof end;
b: for x being set st Q x holds R x @proof end;
for x being set st P x holds R x by a,b;
::> *4
::>
::> 4: This inference is not accepted
Best,
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/
======================================================================