[mizar] Re: what's new in mizar?

[Jesse Alama <alama@stanford.edu>]

Adam Naumowicz <adamn@math.uwb.edu.pl> writes:

> 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

Excellent!  I'm glad to hear that the checker can now handle a wider
class of "obvious" inferences.  Are there cases in the MML where this
really arises?  In other words, if, say, trivdemo is run on the old MML,
do we find any cases where the text could be simplified?

Jesse

-- 
Jesse Alama (alama@stanford.edu)