<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"/>
<description>
<p>The work package is articulated in the following tasks:</p>
<tasks>
- <task name="T2.1">
- <p>XML exportation. The task is devoted to the translation
+ <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).</p>
</task>
- <task name="T2.2">
- <p>Stylesheets to intermediate representation.
- Implementation of a bunch of stylesheets transforming the
+ <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.</p>
</task>
- <task name="T2.3">
- <p>Proof transformation. Similar to the previous task, but
+ <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.</p>
</task>
- <task name="T2.4">
- <p>Automatic extraction of metadata. Relevant metadata such
+ <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
retrieving. The precise list of metadata will be defined
in Work Package 3.</p>
</task>
- <task name="T2.5">
- <p>Presentational Stylesheets. Implementation of a bunch of
+ <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.)</p>
</task>
- <task name="T2.6">
- <p>Automatic Proof Generation in Natural Language. Similar
+ <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
</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"/>
+ <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