|
| bologna | inria | dfki | nijmegen | aei | trusted-logic |
| 13 | 4 | 3 | 11 | 3 | 0 |
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.
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).
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.
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.
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.
Implementation of a bunch of stylesheets transforming the intermediate content representation into a suitable rendering format (MathML presentation, HTML, etc.)
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).
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.
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.
This page is hosted by the
Department of Computer Science,
University of Bologna.
Last updated Fri Feb 2 17:12:30 CET 2007. |
|