Work Package : Transformation
Begin: Month 0
End: Month 21
Contribution of Each Site (in Man Monthes):
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.
Description:The work package is articulated in the following tasks:
T2.1 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).
T2.2 Stylesheets to intermediate representation.
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.
T2.3 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.
T2.4 Automatic extraction of metadata.
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.
T2.5 Presentational Stylesheets.
Implementation of a bunch of
stylesheets transforming the intermediate content
representation into a suitable rendering format (MathML
presentation, HTML, etc.)
T2.6 Automatic Proof Generation in Natural Language.
Automatic Proof Generation in Natural Language.
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).
Milestones and Expected Results:
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
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).
For the end of month 18, we expect to have a first working
prototype of the whole application.