helm/mowgli/home/xml/proposal/innovation.xml

   1 <?xml version="1.0"?>
   2
   3 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
   4
   5 <html>
   6  <head>
   7    <title>Innovation</title>
   8  </head>
   9  <body>
  10
  11  <table width="550">
  12    <tr>
  13     <td>
  14      <a href="contribution.html" target="content"><img src="./../../images/PreviousArrow.gif" width="26" height="26" border="0" alt="Previous Page"/></a>
  15     </td>
  16     <td>
  17      <a href="../project.html" target="content">Index</a>
  18     </td>
  19     <td>
  20      <a href="EC-contribution.html" target="content"><img src="./../../images/NextArrow.gif" width="26" height="26" border="0" alt="Next Page"/></a>
  21     </td>
  22    </tr>
  23   </table>
  24
  25   <br/>
  26
  27   <h1>Innovation</h1>
  28   <p>The main technical novelty of the project is in its synergy of different
  29      scientific communities and research topics: digital libraries, Web
  30      publishing, logical environments.</p>
  31
  32   <img border="0" alt="Architecture" src="./../../images/logo.png" />
  33
  34   <p>From the point of view of Web publishing, our project is the first attempt
  35      to provide a comprehensive description, from content to metadata, of a
  36      given field of knowledge (in our case mathematics), in order to enhance
  37      its accessibility, exchange and elaboration via the World Wide Web. To
  38      this aim, we shall put to use most of the technologies recently introduced
  39      by the W3C: XML, DOM, XSL, XLL, Namespaces, MathML, RDF, etc. From this
  40      respect, the project is first of all a complex test for all these
  41      technologies, and should hopefully become an example of ``best practice''
  42      in their use.  Note that the final architecture is likely to be extendible
  43      to other fields of structured information: the emphasis on mathematics is
  44      motivated by the fact that, due to its complex interplay between content,
  45      structure and notation, it provides a major case study for Web-based
  46      information systems (it is not a case that MathML has been one of few
  47      instances of XML completely developed under the aegis of the World Wide
  48      Web Consortium).</p>
  49   <p>From the point of view of digital libraries, our work is aimed at
  50      exploiting all the potential functionalities offered by the Web, and in
  51      particular a more integrated use of its browsing and searching facilities.
  52      The library is not merely seen as a more or less structured collection of
  53      texts, but as a virtual structure inside which we can freely navigate,
  54      jumping for instance from an entity to its definition, or peeping inside
  55      some information at deeper and deeper levels of details (such as different
  56      levels of detail of a proof).  This is similar to what we currently do
  57      with HTML texts, but in order to enhance the effectiveness of the
  58      consultation, we clearly need a good metadata model of the information.
  59      Moreover, in such an integrated view, it is hardly conceivable to just
  60      apply some ``general purpose'' metadata model (like the Dublin Core
  61      system, say): the metadata model must be eventually specialised to the
  62      actual structure of the information it is supposed to model (and more
  63      structure we have on the information, more relevant metadata we can
  64      usually infer on the document).  For instance, metadata could contain the
  65      whole signature of a given module of mathematical knowledge. The usual
  66      motivation for keeping metadata simple and general is that it is usually
  67      difficult to add this information by hand; but in our case a large part of
  68      the metadata is supposed to be extracted automatically by the (structured)
  69      text itself, allowing for pretty complex metadata models.</p>
  70   <p>Finally, a main aspect of our project is the integration with current
  71      tools for the automation of formal reasoning and mechanisation of
  72      mathematics (proof assistants and logical frameworks). This integration
  73      has a mutual benefit. From the point of view of the mathematical library,
  74      the first and fundamental role of these systems is that of providing
  75      friendly authoring tools (for instance, our ``core'' library will be
  76      automatically extracted from existing libraries of these systems). The
  77      relevance of this point should not be underestimated: as a matter of fact,
  78      the main reason for the failure of complex markup modellings is usually
  79      the lack of suitable authoring tools (it is often painful to add the
  80      markup by hand). Of course, they can also provide other functionalities
  81      (like automatic proof checking) on fragments of the library (typically,
  82      the fragments generated by the tool itself, in its specific logical
  83      dialect). These additional functionalities may be especially relevant for
  84      industrial applications, e.g. in the context of IT security evaluation
  85      standards like the Common Criteria standard (see
  86      <a href="./../publications/others/cc.html">others/cc</a>). In its highest
  87      assurance level, this standard requires the development of formal models
  88      of the IT product under evaluation, as well as mechanized proofs that it
  89      meets its security objectives. Such models and proofs must be published in
  90      a format that can be easily readable and understood by security
  91      evaluators. Hence, there is a strong need from software industry to be
  92      able to produce such documentation directly from the models introduced in
  93      the proof assistant, and to link it with documents describing the IT
  94      product, etc.</p>
  95   <p>On the other side, there is a compelling need of integration between the
  96      current tools for automation of formal reasoning and mechanisation of
  97      mathematics and the most recent technologies for the development of Web
  98      applications and electronic publishing. XML, which is rapidly imposing as
  99      a pivotal technology in the future development of all Internet
 100      applications, and the main tool for representation, manipulation, and
 101      exchange of structured information in the networked age, looks as a
 102      natural, almost mandatory, choice for modelling the information.</p>
 103   <p>In this way, we just obey to the very primitive commandment of the Web:
 104      make your information available.  Currently, libraries in logical
 105      frameworks are usually saved in two formats: a textual one, in the
 106      specific tactical language of the proof assistant, and a compiled (proof
 107      checked) one in some internal, concrete representation language.  Both
 108      representations are obviously unsatisfactory, since they are too oriented
 109      to the specific application: they restrict the access of the libraries to
 110      the users of the given application, and at the same time they are too
 111      sensible to the evolution and the maintenance of the application itself.
 112      On the other side, as soon as the information is put in a standard format
 113      on the Web, <i>any</i> kind of research becomes virtually possible, and
 114      <i>anybody</i> could start developing his own <i>spider</i> for
 115      implementing his own searching requirements. This is clearly a major
 116      improvement w.r.t. the present situation. Currently, you must not only
 117      rely on the searching facilities offered by the specific applications, but
 118      even if you would wish to implement your own searching algorithm, you
 119      would be prevented by the simple reason that the information is not
 120      accessible (in any reasonable sense of the word).</p>
 121   <p>The project builds on the solid ground provided by several existing
 122      XML-based languages for the management of mathematical documents such as
 123      MathML, OpenMath and OMDoc. Each of these markup languages covers a
 124      different aspect of the information. Our aim is not to propose a new
 125      language, but to study and to develop the technological infrastructure
 126      required to integrate all these languages together, in order to take
 127      advantage of the specific features of each of them.</p>
 128
 129  <br/>
 130
 131  <table width="550">
 132    <tr>
 133     <td>
 134      <a href="contribution.html" target="content"><img src="./../../images/PreviousArrow.gif" width="26" height="26" border="0" alt="Previous Page"/></a>
 135     </td>
 136     <td>
 137      <a href="../project.html" target="content">Index</a>
 138     </td>
 139     <td>
 140      <a href="EC-contribution.html" target="content"><img src="./../../images/NextArrow.gif" width="26" height="26" border="0" alt="Next Page"/></a>
 141     </td>
 142    </tr>
 143   </table>
 144
 145  </body>
 146 </html>