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