X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmowgli%2Fhome%2Fxml%2Fwork-packages%2Findex.xml;fp=helm%2Fmowgli%2Fhome%2Fxml%2Fwork-packages%2Findex.xml;h=0000000000000000000000000000000000000000;hb=1696761e4b8576e8ed81caa905fd108717019226;hp=f032a7d9fe659a7f033374ba6e2006d15847051d;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;p=helm.git diff --git a/helm/mowgli/home/xml/work-packages/index.xml b/helm/mowgli/home/xml/work-packages/index.xml deleted file mode 100644 index f032a7d9f..000000000 --- a/helm/mowgli/home/xml/work-packages/index.xml +++ /dev/null @@ -1,121 +0,0 @@ - - - - - - - - - - - - - - - - - - - - -]> - - - - - - - - - - - -

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. -
  2. 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.
    3. -
  3. 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.
    4. -
-

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

- -