--- /dev/null
+<?xml version="1.0"?>
+
+<work-package number="2">
+ <name>Transformation</name>
+ <begin>Month 0</begin>
+ <end>Month 21</end>
+ <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>
+ <dl>
+ <dt>T2.1</dt>
+ <dd>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).</dd>
+
+ <dt>T2.2</dt>
+ <dd>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.</dd>
+
+ <dt>T2.3</dt>
+ <dd>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.</dd>
+
+ <dt>T2.4</dt>
+ <dd>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
+ 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
+ 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
+ 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>
+ </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>
+ <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>
+ </milestone>
+</work-package>
projects / helm.git / blobdiff