helm/mowgli/home/xml/proposal/project-objectives.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>Project Objectives</title>
   8  </head>
   9  <body>
  10   <h1>Project Objectives</h1>
  11   <p>The new frontier of Content Based Information Systems is the so called
  12      ``Semantic Web'' (see
  13      <a href="./../publications/others/w3c_bl98.html">others/w3c_bl98</a>).
  14      Associating meaning with content or establishing a layer of machine
  15      understandable data will allow automated agents, sophisticated search
  16      engines and interoperable services and will enable higher degree
  17      of automation and more intelligent applications.  The ultimate goal of the
  18      Semantic Web is to allow machines to share and exploit knowledge in the
  19      Web way, i.e. without central authority, with few basic rules, in a
  20      scalable, adaptable, extensible manner.  However, the actual development
  21      of the Semantic Web and its technologies has been hindered so far by the
  22      lack of large scale, distributed repositories of structured, content
  23      oriented information. The case of Mathematical knowledge, the most
  24      rigorous and condensed form of knowledge, is paradigmatic.  The World Wide
  25      Web is already now the largest single resource of mathematical knowledge,
  26      and its importance will be exponentiated by the emerging display
  27      technologies like MathML.  However, almost all mathematical documents
  28      available on the Web are marked up only for presentation (in this respect,
  29      current practice in MathML improves on, but does not fundamentally differ
  30      from the older paper-oriented markup schemes like LaTeX or Postscript).
  31      A consequence of this is that the online material is machine-readable, but
  32      not machine-understandable, severely crippling the possibility to offer
  33      added-value services like</p>
  34   <ul>
  35    <li>Preservation of the real informative content in a highly structured and
  36        machine understandable format, suitable for transformation, automatic
  37        elaboration and processing.</li>
  38    <li>Cut and paste on the level of computation (take the output from a Web
  39        search engine and paste it into a computer algebra system).</li>
  40    <li>Automatic proof checking of published proofs.</li>
  41    <li>Semantical search for mathematical concepts (rather than keywords).</li>
  42    <li>Classification: given a concrete mathematical structure, is there a
  43        general theory for it?</li>
  44   </ul>
  45   <p>Due to its rich notational, logical and semantical structure, mathematical
  46      knowledge is thus a main case study for the development of the new
  47      generation of semantic Web systems.  The aim of the proposed project is
  48      both to help in this process, as well as pave the way towards a really
  49      useful virtual, distributed, hyper-textual resource for the working
  50      mathematician, scientist or engineer.  All modern sciences have a
  51      strongly mathematicised core, and will benefit. The real market and
  52      application area for the techniques developed in this project, apart from
  53      the obvious realm of education, lies with high-tech and engineering
  54      corporations that rely on huge formula databases. Currently, both the
  55      content markup as well as the added-value services alluded to above are
  56      very underdeveloped, limiting the usefulness of the vital knowledge. The
  57      infrastructure and knowhow needed for mining this information treasure
  58      and obtaining a competitive edge in development is exactly what we are
  59      attempting to develop in our project.</p>
  60   <p>Several languages have been already proposed for the management of
  61      mathematical information on the Web, both for publishing, communication
  62      and archiving purposes: most notably,
  63      <a href="http://www.w3.org/TR/MathML2/">MathML</a>,
  64      <a href="http://www.nag.co.uk/projects/openmath/omsoc/">OpenMath</a>,
  65      <a href="http://www.mathweb.org/omdoc/">OMDoc</a>. Other languages
  66      must be also considered for definition and specification of Metadata,
  67      such as the <a href="http://purl.org/dc/">Dublin Core</a> System, or
  68      the Resource Description Framework
  69      [<a href="http://www.w3.org/RDF/">RDF</a>].
  70      All these languages, which tend to cover different and orthogonal aspects
  71      of the management of mathematical documents, must be eventually taken into
  72      account for the ambitious goal of our project. One of our aims is actually
  73      the definition of a modular architecture which could exploit the
  74      distinctive potentialities of each one of these languages, integrating
  75      them into a single application.  The integration is in this case
  76      facilitated by the fact that all the languages mentioned are particular
  77      instances of XML, providing the opportunity to use standard XML
  78      technology, and in particular XSL Transformations or
  79      stylesheets [<a href="http://www.w3.org/TR/xslt">XSLT</a>], to pass from
  80      one language to the other.</p>
  81
  82   <img border="0" alt="Architecture" src="./../../images/arch.png" />
  83
  84   <p>The fact of encoding also the microscopic, logical level of mathematics
  85      opens the possibility to have completely formalised subsystems of the
  86      library, which could be checked automatically by standard tools for the
  87      automation of formal reasoning and the mechanisation of mathematics
  88      (proof assistants and logical frameworks, see
  89      <a href="./../publications/others/cup_hp91.html">others/cup_hp91</a> and
  90      <a href="./../publications/others/cup_hp93.html">others/cup_hp93</a>). At
  91      the same time, any of these tools could be used as an authoring system for
  92      documents of the library, by simply exporting their internal libraries
  93      into XML, and using stylesheets to transform the output into a standard,
  94      machine-understandable representation, such as MathML content markup or
  95      OpenMath.</p>
  96   <p>The precise formal content can still be preserved by the machinery of
  97      <a href="http://www.w3.org/TR/xlink/">Xlinks</a>. Moreover, stylesheets
  98      can be also used to solve the annoying notational problem that usually
  99      afflicts formal mathematics, providing a simple way for adding
 100      user-defined styles and notations.</p>
 101
 102     <p>So, our approach leads to a natural integration of proof assistant tools
 103        and the Web. In this integration, the emphasis is just on ``content'':
 104        we do not try to link directly the specific applications to the Web,
 105        that would be a major mistake, for obvious modularity reasons. On the
 106        contrary, we adopt XML as a neutral specification language, and then we
 107        merely work on XML-documents, forgetting the underlying application. In
 108        this way, similar software tools can be applied to different logical
 109        dialects, regardless of their concrete nature. Moreover, if having a
 110        common representation layer is not the ultimate solution to all
 111        inter-operability problems between different applications, it is
 112        however a first and essential step in this direction.  Finally, this
 113        ``standardisation'' process should naturally lead to a substantial
 114        simplification and re-organisation of the current, ``monolithic''
 115        architecture of logical frameworks. All the many different and often
 116        loosely connected functionalities of these complex programs (proof
 117        checking, editing, search and consulting, program extraction, and so on)
 118        could be clearly split in more or less autonomous tasks, and could be
 119        developed by different teams, in totally different languages. This is
 120        the new, ``content-based'' architectural design of future systems.</p>
 121  </body>
 122 </html>