From: Claudio Sacerdoti Coen Date: Wed, 13 Feb 2002 16:25:04 +0000 (+0000) Subject: Another part of the proposal encoded. X-Git-Tag: V_0_3_0_debian_8~331 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2bd5ff76c2328b6ea4c3f6e7a57511496e260e27;p=helm.git Another part of the proposal encoded. --- diff --git a/helm/mowgli/home/xml/work-packages/index.xml b/helm/mowgli/home/xml/work-packages/index.xml index 091b006a4..9d6a5ead9 100644 --- a/helm/mowgli/home/xml/work-packages/index.xml +++ b/helm/mowgli/home/xml/work-packages/index.xml @@ -17,4 +17,90 @@ + +

The previous work packages are not strictly sequential.

+

WP1 should be reasonably short; apart from a few topics requiring a + deeper analysis (Tasks 1.3-5), this phase is essentially meant to rapidly + reach a good level of inter-operability among the different sites.

+

Most part of the work is based on the possibility to have at our + disposal, and as soon as possible, large collections of documents encoded + with semantic markup. One strategy is the import of material (e.g. + journal articles) written in LaTeX. The development of a suitable LaTeX + based authoring tool (Task 4.4) will need to begin immediately, as an + appropriate semantic encoding in LaTeX has to be developed first. + The delivery of the first prototype of the authoring tool is scheduled + for month 18.

+

A more rapid way to get meaningful repositories of fully structured + mathematical knowledge is by exporting them from the available + libraries of Logical Frameworks and Proof Assistants (Task 2.1). + The intelligence contained in the exported XML files should reflect the + requirements defined + in the previous work package, requiring a deep analysis of the markup + model. After six months from the beginning of the project we plan to have + a first prototype of the Exportation Module and a first draft of the + Document Type Descriptor for thelow, logical level. This is our first + Milestone.

+

At this point we may start the study of the intermediate format of the + information, and the implementation of the stylesheets performing the + transformation (tasks T2.2-3). This part of the work is expected to be + essentially completed after one year (second Milestone). Since a strong + feedback is expectedwith presentational issues, we plan to begin the + development of presentational stylesheets around month 9. In turn, the + need of rapidly have at our disposal good presentational engines suggests + to begin their development as soon as possible (task 4.1).

+

In parallel with these transformation issues, we shall start the study and + classification of metadata, and their concrete modelling.

+

Summing up, at the end of first year we plan to have:

+
    +
  • a formal Document Type Descriptor of the intermediate level;
  • +
  • a bunch of stylesheet performing the transformation to intermediate + representation, both for formulae and proofs;
  • +
  • a detailed report on metadata;
  • +
  • a first prototype model of metadata (in RDF format);
  • +
  • a prototype MathML-viewer.
  • +
+

During the first half of second year we shall perform, in parallel, four + major activities:

+
    +
  • study and development of presentational stylesheets, both for expressions + and proofs, and automatic extraction of metadata (tasks T2.4-6).
  • +
  • architectural design and implementation of the consultation engine (task + T4.2, requiring the metadata model), and of the functionalities for + assisted annotation in natural language of the documents (task T4.3, + requiring both the MathML-viewer, and a detailed description of the + intermediate level).
  • +
  • overall architectural design and first prototype implementation of the + distribution model (task T5.1-T5.2).
  • +
  • finalize the first prototype of a LaTeX based authoring tool + (Task 4.4)
  • +
+

The second half of the second year is devoted to the completion of the + previous tasks, and to their integration inside a single, compound + application. Around this time we shall also start a detailed validation + of the application, according to three pilot applications:

+
    +
  1. Formalisation of a full undergraduate course in algebra or analysis for + didactical purposes.
  2. +
  3. Formalization of (part of) the process of loading, verifying and + executing an applet into a smart card. This application will provide + a case study close to both information technology (IT) industry and + Computer Science research, where the presentation and layout needs are + not exactly the same as in Mathematics. The example concerns the + representation of different abstract state machines, transition systems, + typing calculus, and program code. Such concepts are pragmatic use cases + of the formal concepts that usually appears in security evaluations of + IT products and Computer Science articles.
  4. +
  5. Make maximal use of content marked-up articles in a solely + electronic scientific physics journal. This will allow us to demonstrate + the benefits of content mark-up for search, retrieval, and re-use of + mathematical content, and user customisable content presentation. + Several articles will be processed to test scope, functionality, and + user friendliness of the authoring tool developed in Task 4.4. The tool + will be refined and the mathematical semantics covered extended. The + suite of articles will be used to show benefits of automated + annotation and cross-linking between related mathematical concepts.
  6. +
+

The last six months are mainly devoted to testing, debugging, validation, + dissemination of results and exploitation plans.

+
diff --git a/helm/mowgli/home/xsl/work-packages_index.xsl b/helm/mowgli/home/xsl/work-packages_index.xsl index 9ade48c7d..ddd9a035f 100644 --- a/helm/mowgli/home/xsl/work-packages_index.xsl +++ b/helm/mowgli/home/xsl/work-packages_index.xsl @@ -31,9 +31,10 @@ - + +