Hi Freek, On Fri, 22 Sep 2006, Freek Wiedijk wrote:
I guess that Josef's point is that there really two different
levels in "experimenting with Mizar". On the one hand there
is the MML, where more or less everyone can do whatever he/she
likes ("anti-bourabakist", yes, I like that word!) But then
there's also the level of the pascal (delphi?) code of mizf.
Yes.
And here people (even Josef!) cannot do whatever they like (or can he?)
I can, and you (as a member of SUM) can too, probably unless it is published. I actually have published a couple of versions of a modified Mizar verifier in the MoMM distribution, since modifying it (to produce some additional info to get MoMM's advice) was by far the most feasible way for MoMM.
The point is that strictly speaking I don't know how much legal that was. And I also don't know, how much legal it was to include part of (translated) MML into the TPTP library this year. That's why I've been (so far unsuccessfully) trying for a couple of years to clarify what is the Mizar (and MML) licence, and possibly have an open source licence for both (because that makes many things simple). That's also one of the reasons why I have moved the whole production of MPTP from pascal to XSL code (which is mine and open source). And that's also why I have advised Jesse Alama who had the good intent to package Mizar for the Fink packaging system to first ask about it here, because the legal situation is really unclear. It's really quite a bit of pain today.
And yes, you shouldn't be required to be a member of any organisation to do research in formal math.
Best, Josef