[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] the Why project


Hi Freek, Andrzej,
I remember making the Why Mizar environment work with newer MML about a year ago (for Mikolas Janota (http://www.ms.mff.cuni.cz/~janom9am/) experimenting with Why).
I think we discussed this thing a bit at the TYPES summer school, and the suggestion that one of the Adams (I think Grabowski) made was that this kind of articles (small articles serving as a basis for producing computer-generated articles) might be kept in MML. The argument was that this has already happened with another project (cuircuits, I think). This way the article will be kept in sync with MML. 

Best,
Josef

On Mon, 8 May 2006, Freek Wiedijk wrote:


Who is interested in the Why project, and who did the Mizar
stuff for Why?


I am very much interested in Why, although I never really did
something with it.

The Mizar output was added by Jean-Christophe after he had
told me that it was not much work to add output for another
prover.  I don't remember the details, but I think there was a
little article that was needed to support the Mizar code that
was generated by Why.  If so, it is probably part of the Why
distribution.  Jean-Christophe wanted to install that article
into the MML directory when installing Why.  I told him that
that was not the proper thing to do, but we never submitted
this (tiny) article to MML either.

So it would be interesting to know whether the Mizar output
from Why still works with the current version of Mizar.  I
doubt it, really.

Freek