Re: [mizar] PVS GPLed

[Freek Wiedijk <freek@cs.ru.nl>]

Bill:

>Perhaps the people who said that were underestimating how
>difficult it is for someone to learn Mizar when starting
>from zero.

I think this is the problem with Mizar and its documentation.
The people in Bialystok are so used to their system that
they cannot imagine how difficult this is.

Personally I actually think that Mizar is a rather easy
system, but that it just has a few _very_ difficult barriers
that hides this fact quite effectively.  Getting a Mizar
environment right without being an expert is almost
impossible, and finding lemmas in the library also is
almost impossible.  Apart from that the system is quite
easy and nice.

>As I was learning about Mizar, the one document that helped
>me the most was Michal Muzalewski's paper from 1993,
>"An Outline of PC Mizar".  The paper is still an excellent
>resource, although it does not reflect many changes in Mizar
>that have occurred since 1993.  If only someone had the
>time to revise that document...  If I remember correctly,
>I found the paper through a link from Freek's web page.

<http://www.cs.ru.nl/~freek/mizar/mizarmanual.pdf>, I think.

Freek