]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/mowgli/home/xml/work-packages/index.xml
ocaml 3.09 transition
[helm.git] / helm / mowgli / home / xml / work-packages / index.xml
index 091b006a4d88072af2c154e052e8352be24ef7de..f032a7d9fe659a7f033374ba6e2006d15847051d 100644 (file)
@@ -1,11 +1,26 @@
 <?xml version="1.0"?>
 
 <!DOCTYPE work-packages [
- <!ELEMENT work-packages (work-package+)>
+ <!ELEMENT work-packages (work-package+,description)>
 
  <!ELEMENT work-package EMPTY>
  <!ATTLIST work-package
            file CDATA #REQUIRED>
+
+ <!ELEMENT description (p|dl|ul|ol)+>
+
+ <!-- A subset of XHTML -->
+ <!ELEMENT p (#PCDATA|em|a)*>
+ <!ELEMENT em (#PCDATA)>
+ <!ELEMENT a (#PCDATA)>
+ <!ATTLIST a
+           href CDATA #REQUIRED>
+ <!ELEMENT dl (dt|dd)+>
+ <!ELEMENT dt (#PCDATA)>
+ <!ELEMENT dd (#PCDATA)>
+ <!ELEMENT ul (li)+>
+ <!ELEMENT ol (li)+>
+ <!ELEMENT li (#PCDATA)>
 ]>
 
 <work-packages>
  <work-package file="distribution"/>
  <work-package file="testing-and-validation"/>
  <work-package file="information-dissemination-and-exploitation"/>
+ <description>
+  <p>The previous work packages are not strictly sequential.</p>
+  <p> 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.</p>
+  <p>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.</p>
+  <p>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.</p>
+  <p>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).</p>
+  <p>In parallel with these transformation issues, we shall start the study and
+     classification of metadata, and their concrete modelling.</p>
+  <p>Summing up, at the end of first year we plan to have:</p>
+  <ul>
+   <li>a formal Document Type Descriptor of the intermediate level;</li>
+   <li>a bunch of stylesheet performing the transformation to intermediate
+       representation, both for formulae and proofs;</li>
+   <li>a detailed report on metadata;</li>
+   <li>a first prototype model of metadata (in RDF format);</li>
+   <li>a prototype MathML-viewer.</li>
+  </ul>
+  <p>During the first half of second year we shall perform, in parallel, four
+     major activities:</p>
+  <ul>
+   <li>study and development of presentational stylesheets, both for expressions
+       and proofs, and automatic extraction of metadata (tasks T2.4-6).</li>
+   <li>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).</li>
+   <li>overall architectural design and first prototype implementation of the
+       distribution model (task T5.1-T5.2).</li>
+   <li>finalize the first prototype of a LaTeX based authoring tool
+       (Task 4.4)</li>
+  </ul>
+  <p>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:</p>
+  <ol>
+   <li>Formalisation of a full undergraduate course in algebra or analysis for
+       didactical purposes.</li>
+   <li>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.</li>
+   <li>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.</li>
+  </ol>
+  <p>The last six months are mainly devoted to testing, debugging, validation,
+     dissemination of results and exploitation plans.</p>
+ </description>
 </work-packages>