Re: [mizar] MML License

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Hi Freek,

On Sat, 15 Mar 2003, Freek Wiedijk wrote:

> For a contrasting data point, note that PVS is the most
> popular proof assistant of today, and it is very much
> copyrighted, and its source is certainly _not_ easily
> obtainable too (it took me half a year to get a license).

Theorem provers that do not provide their source code are not even allowed 
into the annual CASC provers' competition (see 
http://www.cs.miami.edu/~tptp/CASC/18/Design.html#SystemDelivery ).

See http://www.cs.miami.edu/~tptp/CASC/18/SystemInfo
for list of last CASC participants.

As for proof assistants, if we take your sample of 15 assistants ( 
http://link.springer.de/link/service/series/0558/papers/2594/25940188.pdf),
then only Mizar, PVS and Nuprl5 provide binary and no source (Nuprl5's manual 
http://www.cs.cornell.edu/Info/Projects/NuPrl/html/02cucs-NuprlManual-03starting.pdf
promises the source when it gets stable).
Theorema provides neither binary nor source.

"PVS being the most popular assistant" seems a bit strong assertion, could 
you explain why you think so? 
Do you think that could be strengthened to "the most popular assistant 
for writing formalized math"?

Regards,
Josef