This commit was manufactured by cvs2svn to create branch 'moogle'.

[helm.git] / helm / mowgli / home / xml / work-packages / transformation.xml

diff --git a/helm/mowgli/home/xml/work-packages/transformation.xml b/helm/mowgli/home/xml/work-packages/transformation.xml
deleted file mode 100644 (file)
index 972abe1..0000000
--- a/helm/mowgli/home/xml/work-packages/transformation.xml
+++ /dev/null
@@ -1,105 +0,0 @@
-<?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"/>
- <person-month participant="nijmegen" number="11"/>
- <person-month participant="aei" number="3"/>
- <person-month participant="trusted-logic" number="0"/>
- <objectives>
-  <p>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.</p>
- </objectives>
- <description>
-  <p>The work package is articulated in the following tasks:</p>
-  <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).</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.</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.</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.</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.)</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).</p>
-   </task>
-  </tasks>
- </description>
- <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,
-     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.</p>
-  <p>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).</p>
-  <p>For the end of month 18, we expect to have a first working
-     prototype of the whole application.</p>
- </milestones>
-</work-package>