[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] PVS GPLed
Wow, I'm surprised by how much discussion followed from my comments.
That's a good thing, I think.
I have read about the policy of making the sources available to those
who have written Mizar articles. I was not sure whether that policy
is still in effect. I'm glad to hear that it is. I would like to
write a Mizar article, so perhaps I will be able get access under
that policy. It's still an open question whether I can actually write
an article that the committee would want to include in the MML.
> >The correct parse tree can actually be *changed* by adding
> >or removing functor definitions.
>
> No. The parse tree will be the same. The interpretation of
> the symbols will change, but the parse tree will be the same.
I'll post an example (soon) showing what I meant by this remark.
To me, it looks like the parse tree is changing, but perhaps there
is another explanation for what happens. I'll post the example under
a new title: "Question about functor precedence."
> I once started such a manual. My "tutorial" ("... in nine
> easy steps") was supposed to be part of it. But no one in
> the Mizar group seemed to think it would be useful (which I
> still find very strange!), and by now I don't think I ever
> will write it.
I have read your tutorial. I don't know why some people said it
would not be useful. I found it helpful. Perhaps the people who said
that were underestimating how difficult it is for someone to learn
Mizar when starting from zero. I applaud everyone who has written
materials to help new Mizar users. Many thanks, Freek!
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.
Bill