Re: [mizar] Strong Mizar wish: linking to consider (fwd)

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

> as soon as you agree on some DTD for Mizar and export
> Mizar documents into XML, we would
> be VERY interested to work on them, 

I think it is still going to take some time. Also, the extent of using XML 
for internal purposes has to be determined and probably experimented with 
a little.


> applying our HELM
> technology and knowhow (e.g. for rendering, or for
> the implementation of complex searching and retrieving
> functionalities).

Grzegorz Bancerek is also working on MML Query 
(http://megrez.mizar.org/services/query/). I think it is not finished 
yet, but already very useful.
I fear a bit, that specialised search/presentation services tailored to 
each system's logic (like MML Query for Mizar, HELM for Coq, or perhaps 
MBase for Omega) are more useful to the users, than systems trying to 
contain everything. 
But certainly, it makes sense to have some integration and reuse some 
common tools.

Regards,
Josef Urban