helm/mowgli/home/xml/work-packages/transformation.xml

   1 <?xml version="1.0"?>
   2
   3 <!DOCTYPE work-package SYSTEM "work-package.dtd">
   4
   5 <work-package number="2">
   6  <name>Transformation</name>
   7  <begin>Month 0</begin>
   8  <end>Month 21</end>
   9  <leader file="bologna/sacerdoti"/>
  10  <person-month participant="bologna" number="13"/>
  11  <person-month participant="inria" number="4"/>
  12  <person-month participant="dfki" number="3"/>
  13  <person-month participant="nijmegen" number="11"/>
  14  <person-month participant="aei" number="3"/>
  15  <person-month participant="trusted-logic" number="0"/>
  16  <objectives>
  17   <p>This work package is devoted to the complex issue of
  18      transforming a low level, content description of mathematics
  19      (understandable by automatic applications for the
  20      mechanization of mathematics) into a human-readable
  21      presentational format. It covers both statements and proofs.
  22      The transformation will be decomposed in a sequence of
  23      intermediate steps, for modularity reasons. All
  24      transformations will be implemented by means of
  25      XSLT-stylesheets. Stylesheets will be simple, modular, and
  26      easily composable. All the transformation process should be
  27      independent from any specific application.</p>
  28  </objectives>
  29  <description>
  30   <p>The work package is articulated in the following tasks:</p>
  31   <tasks>
  32    <task id="T2.1">
  33     <name>XML exportation.</name>
  34     <p>The task is devoted to the translation
  35        of the standard library of the COQ Proof assistant into a
  36        suitable XML dialect, and to the definition of a low-level
  37        DTD for the terms of the Calculus of Inductive
  38        Construction (the logical system used by COQ).</p>
  39    </task>
  40    <task id="T2.2">
  41     <name>Stylesheets to intermediate representation.</name>
  42     <p>Implementation of a bunch of stylesheets transforming the
  43        low-level logical description of COQ-expressions into a
  44        ``standard'' intermediate, content-level representation
  45        such as MathML content.</p>
  46    </task>
  47    <task id="T2.3">
  48     <name>Proof transformation.</name>
  49     <p>Similar to the previous task, but
  50        for proofs. The delicate point, here, is the fact that no
  51        ``standard'' intermediate representation currently exists,
  52        and thus it has to be defined.</p>
  53    </task>
  54    <task id="T2.4">
  55     <name>Automatic extraction of metadata.</name>
  56     <p>Relevant metadata such
  57        as list of identifiers in critical positions inside
  58        statements can be automatically extracted from the fully
  59        structured representation of mathematical objects. This
  60        information can then be exploited for searching and
  61        retrieving. The precise list of metadata will be defined
  62        in Work Package 3.</p>
  63    </task>
  64    <task id="T2.5">
  65     <name>Presentational Stylesheets.</name>
  66     <p>Implementation of a bunch of
  67        stylesheets transforming the intermediate content
  68        representation into a suitable rendering format (MathML
  69        presentation, HTML, etc.)</p>
  70    </task>
  71    <task id="T2.6">
  72     <name>Automatic Proof Generation in Natural Language.</name>
  73     <p>Similar
  74        to the previous task but for proofs. In this case, a fully
  75        automated approach is unlikely to produce really
  76        satisfactory results, and the process should be possibly
  77        integrated with some mechanism for interactive annotation
  78        (see Task 4.3).</p>
  79    </task>
  80   </tasks>
  81  </description>
  82  <deliverable file="transformation/d2a"/>
  83  <deliverable file="transformation/d2b"/>
  84  <deliverable file="transformation/d2c"/>
  85  <deliverable file="transformation/d2d"/>
  86  <deliverable file="transformation/d2e"/>
  87  <deliverable file="transformation/d2f"/>
  88  <deliverable file="transformation/d2g"/>
  89  <milestones>
  90   <p>The exportation module D2.a. is our first
  91      milestone: without a large amount of available documents it
  92      would be impossible to test the transformations. Similarly,
  93      without a precise definition of the intermediate language,
  94      and a large sample of documents in this format (D2c-d) we
  95      cannot start to seriously address the presentational issue.
  96      Note that the intermediate language is the real core of the
  97      whole project.</p>
  98   <p>The development of presentational stylesheets also depends
  99      in an essential way on the development of rendering/browsing
 100      engines for the chosen presentational language (in
 101      particular, for MathML).</p>
 102   <p>For the end of month 18, we expect to have a first working
 103      prototype of the whole application.</p>
 104  </milestones>
 105 </work-package>