The work package is articulated in the following tasks:
XML exportation. The task is devoted to the translation
+ 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). Stylesheets to intermediate representation.
- Implementation of a bunch of stylesheets transforming the
+ 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. Proof transformation. Similar to the previous task, but
+ 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. Automatic extraction of metadata. Relevant metadata such
+ 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
@@ -57,14 +61,16 @@
retrieving. The precise list of metadata will be defined
in Work Package 3. Presentational Stylesheets. Implementation of a bunch of
+ Implementation of a bunch of
stylesheets transforming the intermediate content
representation into a suitable rendering format (MathML
presentation, HTML, etc.) Automatic Proof Generation in Natural Language. Similar
+ 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
@@ -73,13 +79,13 @@
The exportation module D2.a. is our first milestone: without a large amount of available documents it