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