[mizar] Re: Mizar Parser

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Andrea Asperti wrote:

> Dear Andrzej and Czeslaw,
>
>         you did not answer yet to my offer of
> exporting the "internal structure" of Mizar into
> XML. Our aim is exactly to bypass the textual
> parsing that in the case of Mizar looks particularly
> complex (we also hope that the the internal
> representation is a bit more stable than the syntax).
> The kind of work we plan to explore then is:
>
> 1. to rebuild an hypertextual vernacular-like presentation,
> as close as possible to the input. The intended output
> would be html/mathml, and all the transformations would
> be performed via XSLT stylsheets.
>
> 2. building functionalities for searching/retrieving
> logical items inside the library, explicitating
> dependencies, etc. Here we have some tools we are
> developing for Coq, and we would like to test on a
> different repository of mathematical documents.
> We also made some experiments with Nuprl, already.
>
> We would NOT be interested in the proof-checking part,
> so there would be no overlapping with the existing
> tools.
>
> Please, let me know if this makes sense to you, and
> if you are interested.
>
> I will be on holiday for the next 20 days, but I
> would really appreciate to have an answer before
> I am back: we are a small group, and we have to plan
> our future work with some advance.
>
> Looking forward for your answer I send you my best
> wishes.
>
>                                 -- andrea
>
> P.S. If you think that, following the recent debate,
> my messages had to be posted in the
> Mizar-forum, please do it, I do not mind.