X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmowgli%2Fhome%2Fxml%2Fwork-packages%2Ftransformation.xml;h=972abe1a2bc3cf4f52ac8507490d26f9a85fce17;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=1cffe28a322733b7450513e0c6d98aa4ad6b0fd5;hpb=d8ad1d26122af00feda930086b6cfa42de0139fe;p=helm.git diff --git a/helm/mowgli/home/xml/work-packages/transformation.xml b/helm/mowgli/home/xml/work-packages/transformation.xml index 1cffe28a3..972abe1a2 100644 --- a/helm/mowgli/home/xml/work-packages/transformation.xml +++ b/helm/mowgli/home/xml/work-packages/transformation.xml @@ -1,9 +1,12 @@ + + Transformation Month 0 Month 21 + @@ -25,59 +28,65 @@

The work package is articulated in the following tasks:

-
-
T2.1
-
XML exportation. The task is devoted to the translation + + + 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).

- -
T2.2
-
Stylesheets to intermediate representation. - Implementation of a bunch of stylesheets transforming the + 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.

- -
T2.3
-
Proof transformation. Similar to the previous task, but + 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.

- -
T2.4
-
Automatic extraction of metadata. Relevant metadata such + 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.

- -
T2.5
-
Presentational Stylesheets. Implementation of a bunch of + 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.)

- -
T2.6
-
Automatic Proof Generation in Natural Language. Similar + 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).

-
+ (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, @@ -92,5 +101,5 @@ particular, for MathML).

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

-
+