]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/mowgli/home/xml/work-packages/transformation.xml
ocaml 3.09 transition
[helm.git] / helm / mowgli / home / xml / work-packages / transformation.xml
index 1cffe28a322733b7450513e0c6d98aa4ad6b0fd5..972abe1a2bc3cf4f52ac8507490d26f9a85fce17 100644 (file)
@@ -1,9 +1,12 @@
 <?xml version="1.0"?>
 
+<!DOCTYPE work-package SYSTEM "work-package.dtd">
+
 <work-package number="2">
  <name>Transformation</name>
  <begin>Month 0</begin>
  <end>Month 21</end>
+ <leader file="bologna/sacerdoti"/>
  <person-month participant="bologna" number="13"/>
  <person-month participant="inria" number="4"/>
  <person-month participant="dfki" number="3"/>
  </objectives>
  <description>
   <p>The work package is articulated in the following tasks:</p>
-  <dl>
-   <dt>T2.1</dt>
-   <dd>XML exportation. The task is devoted to the translation
+  <tasks>
+   <task id="T2.1">
+    <name>XML exportation.</name>
+    <p>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).</dd>
-
-   <dt>T2.2</dt>
-   <dd>Stylesheets to intermediate representation.
-       Implementation of a bunch of stylesheets transforming the
+       Construction (the logical system used by COQ).</p>
+   </task>
+   <task id="T2.2">
+    <name>Stylesheets to intermediate representation.</name>
+    <p>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.</dd>
-
-   <dt>T2.3</dt>
-   <dd>Proof transformation. Similar to the previous task, but
+       such as MathML content.</p>
+   </task>
+   <task id="T2.3">
+    <name>Proof transformation.</name> 
+    <p>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.</dd>
-
-   <dt>T2.4</dt>
-   <dd>Automatic extraction of metadata. Relevant metadata such
+       and thus it has to be defined.</p>
+   </task>
+   <task id="T2.4">
+    <name>Automatic extraction of metadata.</name> 
+    <p>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.</dd>
-
-   <dt>T2.5</dt>
-   <dd>Presentational Stylesheets. Implementation of a bunch of
+       in Work Package 3.</p>
+   </task>
+   <task id="T2.5">
+    <name>Presentational Stylesheets.</name> 
+    <p>Implementation of a bunch of
        stylesheets transforming the intermediate content
        representation into a suitable rendering format (MathML
-       presentation, HTML, etc.)</dd>
-
-   <dt>T2.6</dt>
-   <dd>Automatic Proof Generation in Natural Language. Similar
+       presentation, HTML, etc.)</p>
+   </task>
+   <task id="T2.6">
+    <name>Automatic Proof Generation in Natural Language.</name> 
+    <p>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).</dd>
-  </dl>
+       (see Task 4.3).</p>
+   </task>
+  </tasks>
  </description>
- <deliverable file="D2.a"/>
- <deliverable file="D2.b"/>
- <deliverable file="D2.c"/>
- <deliverable file="D2.d"/>
- <deliverable file="D2.e"/>
- <deliverable file="D2.f"/>
- <deliverable file="D2.g"/>
- <milestone>
+ <deliverable file="transformation/d2a"/>
+ <deliverable file="transformation/d2b"/>
+ <deliverable file="transformation/d2c"/>
+ <deliverable file="transformation/d2d"/>
+ <deliverable file="transformation/d2e"/>
+ <deliverable file="transformation/d2f"/>
+ <deliverable file="transformation/d2g"/>
+ <milestones>
   <p>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,
      particular, for MathML).</p>
   <p>For the end of month 18, we expect to have a first working
      prototype of the whole application.</p>
- </milestone>
+ </milestones>
 </work-package>