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