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

[Andrea Asperti <asperti@CS.UniBO.IT>]

> 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. 

It could be true. For the moment I would be already 
happy to
reach some agreement on the representation of 
mathematical EXPRESSIONS. The markup at this level 
is defined by what you are trying to encode, 
and not by the way it is internally encoded. 
MathML-content provides a good starting point, but we
must definitely go beyond the K-12 fragment.
Our main point is that the definition of this layer
should be conceived as a collaborative process of
the entire community interested in these arguments.
We should try to set up a reasobale way to reach 
this goal (I am currently trying to push this point
of view inside the MathML WG).

Secondly, if you are interested in web publishing, 
the transformation from content to presentation is
likely to be done by means of stylesheets. Again, 
the development of such stylesheets can and should
be conceived as a collaborative process. 

I think we should try to identify who is currently 
interested in these arguments in the world and
to set up a suitable collaborative environment among
all interested parties.

Of course this is not the end of the story, but is
an important piece of it. 

Regards.
				-- andrea