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

[Claudio Sacerdoti Coen <sacerdot@CS.UniBO.IT>]

 Hi,

> > The first stage that is currently discussed, is using XML as an internal
> > format for various Mizar files. Once this is done, we can think of export
> > to other formats, be it HELM or OMDoc. I did not find any DTDs on the
> > MOWGLI page ... maybe I missed something?

 The MOWGLI project has just started (we had the kick-off a few days ago)
 and will be developed in the next three years. The HELM project, instead,
 is older and already quite developed.

> I am not sure that the HELM format is a good format to transform into,
> since it is very oriented towards the internal data format in Coq. I
> understood Claudio's remark as "first use some XML-format for Mizar" just
> as Coq uses the HELM format, which I think is very reasonable.

 Exactly (even if it is not the end of the story):

 In the HELM architecture there are at least two different XML levels.
 The first one is system-dependent (it is in fact just logic-dependent,
 which is much better). This level just encodes in XML all the useful
 information present in the internal format of the system. The information
 is useful if it is possible to parse that information and perform
 proof-checking on it. So, if you use XML as an internal format for various
 Mizar file, the DTD will just play the same role as our DTD for Coq.

 The second level is the content level (i.e. a level based on MathML
 content + some encoding for the proof steps). At this level many
 different encodings can be exploited: plain MathML Content,
 MathML Content + something else, OpenMath, OMDoc, etc.
 What we do in HELM is providing some XSLT stylesheets to map the logical
 level to the content level. The idea is that for every system the logical
 level is different, but the content level can be shared.

 Finally, we provide utilites to work on both levels. As an example, we
 provide stylesheets to go from the content level to a presentational level,
 which can be dynamic HTML or MathML presentation. We also provide tools
 to apply the transformations on-line, tools to manage the distribution of
 the information, tools to extract/describe/render metadata informations,
 tools to draw graph of dependencies between theorems and definitions, etc.
 All the latest tools are completely logic-independent and so we hope to
 reuse them as they are for other systems different from Coq.


						Regards,
						 C.S.C.

-- 
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
PhD Student in Computer Science at University of Bologna
E-mail: sacerdot@cs.unibo.it
http://caristudenti.cs.unibo.it/~sacerdot
----------------------------------------------------------------