X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fmowgli%2Fhome%2Fxml%2Fwork-packages%2Ftransformation.xml;fp=helm%2Fmowgli%2Fhome%2Fxml%2Fwork-packages%2Ftransformation.xml;h=0000000000000000000000000000000000000000;hp=972abe1a2bc3cf4f52ac8507490d26f9a85fce17;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1 diff --git a/helm/mowgli/home/xml/work-packages/transformation.xml b/helm/mowgli/home/xml/work-packages/transformation.xml deleted file mode 100644 index 972abe1a2..000000000 --- a/helm/mowgli/home/xml/work-packages/transformation.xml +++ /dev/null @@ -1,105 +0,0 @@ - - - - - - Transformation - Month 0 - Month 21 - - - - - - - - -

This work package is devoted to the complex issue of - transforming a low level, content description of mathematics - (understandable by automatic applications for the - mechanization of mathematics) into a human-readable - presentational format. It covers both statements and proofs. - The transformation will be decomposed in a sequence of - intermediate steps, for modularity reasons. All - transformations will be implemented by means of - XSLT-stylesheets. Stylesheets will be simple, modular, and - easily composable. All the transformation process should be - independent from any specific application.

- - -

The work package is articulated in the following tasks:

- - - XML exportation. -

The task is devoted to the translation - of the standard library of the COQ Proof assistant into a - suitable XML dialect, and to the definition of a low-level - DTD for the terms of the Calculus of Inductive - Construction (the logical system used by COQ).

- - - Stylesheets to intermediate representation. -

Implementation of a bunch of stylesheets transforming the - low-level logical description of COQ-expressions into a - ``standard'' intermediate, content-level representation - such as MathML content.

- - - Proof transformation. -

Similar to the previous task, but - for proofs. The delicate point, here, is the fact that no - ``standard'' intermediate representation currently exists, - and thus it has to be defined.

- - - Automatic extraction of metadata. -

Relevant metadata such - as list of identifiers in critical positions inside - statements can be automatically extracted from the fully - structured representation of mathematical objects. This - information can then be exploited for searching and - retrieving. The precise list of metadata will be defined - in Work Package 3.

- - - Presentational Stylesheets. -

Implementation of a bunch of - stylesheets transforming the intermediate content - representation into a suitable rendering format (MathML - presentation, HTML, etc.)

- - - Automatic Proof Generation in Natural Language. -

Similar - to the previous task but for proofs. In this case, a fully - automated approach is unlikely to produce really - satisfactory results, and the process should be possibly - integrated with some mechanism for interactive annotation - (see Task 4.3).

- - - - - - - - - - - -

The exportation module D2.a. is our first - milestone: without a large amount of available documents it - would be impossible to test the transformations. Similarly, - without a precise definition of the intermediate language, - and a large sample of documents in this format (D2c-d) we - cannot start to seriously address the presentational issue. - Note that the intermediate language is the real core of the - whole project.

-

The development of presentational stylesheets also depends - in an essential way on the development of rendering/browsing - engines for the chosen presentational language (in - particular, for MathML).

-

For the end of month 18, we expect to have a first working - prototype of the whole application.

- -