3 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
7 <title>Innovation</title>
14 <a href="contribution.html" target="content"><img src="./../../images/PreviousArrow.gif" width="26" height="26" border="0" alt="Previous Page"/></a>
17 <a href="../project.html" target="content">Index</a>
20 <a href="EC-contribution.html" target="content"><img src="./../../images/NextArrow.gif" width="26" height="26" border="0" alt="Next Page"/></a>
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>
32 <img border="0" alt="Architecture" src="./../../images/logo.png" />
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
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
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>
134 <a href="contribution.html" target="content"><img src="./../../images/PreviousArrow.gif" width="26" height="26" border="0" alt="Previous Page"/></a>
137 <a href="../project.html" target="content">Index</a>
140 <a href="EC-contribution.html" target="content"><img src="./../../images/NextArrow.gif" width="26" height="26" border="0" alt="Next Page"/></a>