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=ac1e6d89c19c875a334c7f8bbb7d5107067c3a44;hpb=2ba3d3b802bfa9ca330f1dc2e54653b3bcceba65;p=helm.git diff --git a/helm/mowgli/home/xml/work-packages/transformation.xml b/helm/mowgli/home/xml/work-packages/transformation.xml index ac1e6d89c..972abe1a2 100644 --- a/helm/mowgli/home/xml/work-packages/transformation.xml +++ b/helm/mowgli/home/xml/work-packages/transformation.xml @@ -6,6 +6,7 @@ Transformation Month 0 Month 21 + @@ -28,28 +29,31 @@

The work package is articulated in the following tasks:

- -

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

- -

Stylesheets to intermediate representation. - Implementation of a bunch of stylesheets transforming the + + 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 + + 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 + + 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 @@ -57,14 +61,16 @@ retrieving. The precise list of metadata will be defined in Work Package 3.

- -

Presentational Stylesheets. Implementation of a bunch of + + 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 + + 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 @@ -73,13 +79,13 @@ - - - - - - - + + + + + + +

The exportation module D2.a. is our first milestone: without a large amount of available documents it