4 <!ELEMENT consortium (site+,description)>
8 <!ELEMENT description (p|dl|ul|ol)+>
10 <!-- A subset of XHTML -->
11 <!ELEMENT p (#PCDATA|em|a)*>
12 <!ELEMENT em (#PCDATA)>
13 <!ELEMENT a (#PCDATA)>
16 <!ELEMENT dl (dt|dd)+>
17 <!ELEMENT dt (#PCDATA)>
18 <!ELEMENT dd (#PCDATA)>
21 <!ELEMENT li (#PCDATA)>
25 <site file="bologna"/>
28 <site file="nijmegen"/>
30 <site file="trusted-logic"/>
32 <p>The Consortium has been built with the aim to join some essential
33 knowhow in different areas of I.T. related to the creation and
34 maintenance of a digital library of structured mathematical knowledge.</p>
36 <p>MOWGLI is meant to develop the technological infrastructure required to
37 integrate existing Markup languages and standards such as
38 <a href="http://www.w3.org/Math/">MathML</a>,
39 <a href="http://www.openmath.org">OpenMath</a> or
40 <a href="http://www.mathweb.org/omdoc/">OMDoc</a>,
41 covering different aspects of mathematical
42 intelligence, into a single application.
43 Expertise on these languages and the related technologies is
44 respectively provided by the following partners:</p>
47 <dd>Department of Computer Science, University of Bologna,
48 member of the World Wide Web Consortium and of the W3C Working Group
49 on MathML; Lemme-Project at INRIA Sophia-Antipolis.</dd>
52 <dd>University of Eindhoven (sub-site of Nijmegen):
53 Professor Arjeh Cohen is one of the leaders of the
54 OpenMath initiative, and MOWGLI is expected to take the maximum profit
55 from the successful OpenMath Esprit project, no.24969.</dd>
58 <dd>DFKI. Dr.Michael Kohlhase is the main
59 auhtor of OMDoc; DFKI has a long research tradition in the management of
60 mathematical knowledge bases, metadata, searching and retrieval
64 <p>More generally, the Department of Computer Science in Bologna has a
65 long experience in XML-related technology, and in particular in their
66 application to the particular domain of mathematical developments,
68 <a href="http://www.cs.unibo.it/helm">``Hypertextual Electronic Library
69 of Mathematics'' (HELM) Project</a>. A main
70 component of HELM is the
71 <a href="http://www.cs.unibo.it/helm/mml-widget/index.html">GtkMathView
72 widget</a>, a C++ rendering engine for MathML that will be distributed as
73 an official package of the next Debian release of Linux.</p>
75 <p>Similarly, the Lemme Project in Sophia-Antipolis has a large experience of
76 edition of mathematical objects. It develops the graphical environment
77 Pcoq, dedicated to the development of mathematical proofs, using the
78 Coq proof assistant. Among many features, Pcoq has a sophisticated two
79 dimensional formula and natural language proof edition component,
80 allowing intuitive and powerful interactions. Built on the Figue
81 environment, Pcoq can be made compatible with MathML. The Pcoq interface
82 is intensively used by teams whose research activity concerns
83 the certification of mathematical algorithms.</p>
85 <p>DFKI will contribute requirements and metadata from the
86 viewpoint of educational applications including search
87 functionalities. It will actively work on presentational transformations,
88 the generation of proofs in natural language as well as on knowledge bases
89 for mathematical knowledge DFKI intends to exploit the results of the
90 MOWGLI project in pilot applications in current and planned research and
91 in projects for the prototypical implementation of intelligent
92 environments for learning of mathematics. In particular, the knowledge
93 representation for mathematics on the Web is important for such Web-based
94 systems. Knowledge bases that provide a common repository and ontology for
95 mathematical knowledge are indispensible in systems that integrate various
96 systems working on mathematical knowledge. DFKI also has a fierce interest
97 in pushing and leveraging the quality of standardisation efforts within
98 the worldwide initiative of the Semantic Web education systems and
99 electronic publishing.</p>
101 <p>In order to immediately dispose of a large repository of structured
102 mathematical information, the consortium comprises the developers of
103 one of the most successful proof assistant tools currently
104 available: the <a href="http://pauillac.inria.fr/coq/">Coq</a> proof
105 engine of INRIA-Rocquencourt.
106 The Coq standard library includes more than thousand lemmas and theorems
107 and the whole number of statements proved by users is evaluated to
108 hundred thousands, covering arithmetics, algebra, analysis and
109 computer science. We expect to integrate the current different ways of
110 browsing, searching and rendering Coq mathematical developments into a
111 coherent and Web-oriented architecture open to the Coq user community
114 <p>An alternative route for the creation of content-based mathematical
115 information from standard digital repositories by means of a suitable
116 LaTeX-based authoring system will be explored by the Albert
117 Einstein Institute (AEI) in Golm (Germany). AEI publishes a solely
118 electronic review journal, <em>Living Reviews in Relativity</em> on
119 the Web, which provides refereed, regularly updated review
120 articles on all areas of gravitational physics. Since its
121 release in January 1998 the journal has become a primary
122 entry point for students, lecturers and researchers alike
123 for up-to-date information on the current status of research
124 in gravitational physics. Moving this unique repository and
125 communication forum of current physical and mathematical
126 knowledge in relativity to content mark-up, making it
127 available for semantic search, and for re-use and evaluation
128 e.g. in math algebra systems motivates the involvement
129 in the MOWGLI project. The journal will develop a
130 LaTeX based authoring tool interfacing with MOWGLI, and
131 serve as a showcase to demonstrate how content-mark-up in
132 mathematics improves the usability and information depth
133 of electronic science journals.</p>
135 <p>The AEI will be supported by the newly founded Center for Information
136 Management (CIM) of the Max Planck Society. The CIM has been set up
137 by the Society to support researchers and research processes in the area
138 of information management. The objectives of the project include
139 coordination of existing activities within the Society and
140 implementation of a strategy to develop electronic research archives.
141 The current Managing Editor of the AEI's electronic journal Living
142 Reviews in Relativity has been appointed executive director of the CIM
143 (starting from 1 Sep 2001) and will be in charge of the project management
144 for Tasks 4.4 and 6.3 of the proposal. The CIM will be in an
145 excellent position to promote dissemination and use of the project results
146 within the Max Planck Society. It will further give technical support to
147 the Dissemination Manager in providing the MOWGLI website.</p>
149 <p>Professor Wegner, Scientific Coordinator of EMIS (European
150 Mathematical Information Service), will also provide a main liaison with
151 previous and successful European Projects on digital libraries and
152 metadata, such as <a href="http://www.emis.de/projects/EULER">EULER</a>
153 and the TRIAL Solution project (\verb+http://www.trial-solution.de+).
154 In particular, all the achievements of these Projects
155 will be integrated inside MOWGLI, as far as the respective teams
157 Moreover, in his quality of Scientific Coordinator of EMIS, member
158 of the advisory board for MATHDI, and Chairman of the Electronic
159 Publishing Committee of European
160 Mathematical Society, Professor Wegner is an excellent candidate
161 to organise the information
162 dissemination and exploitation activities for the project.</p>
164 <p>In particular, the Department of Computer Science of the University of
165 Nijmegen will apply MOWGLI's technologies to the development of
166 an ``electronic book'', covering a typical undergraduate course
167 in Algebra or Analysis. The Department of Computer Science in Nijmegen
168 has a lot of experience in formal mathematics and theorem proving.
169 Notably, the group has done large theory developments in the theorem
170 prover Coq. (The <a href="http://www.cs.kun.nl/gi/projects/fta/">FTA
171 project</a>: Eindhoven University of Technology, a sub-site of Nijmegen,
172 has expertise in OpenMath and in using WWW technology for educational
173 purposes. This has resulted -- among other things -- in
174 <a href="http://www.win.tue.nl/~ida/">IDA</a>, the
175 interactive course notes in algebra where a combination of HTML
176 and applets is used to present the mathematics. Jointly, Nijmegen and
177 Eindhoven have experience in combining theorem provers and computer
178 algebra packages, notably Coq and GAP.</p>
180 <p>Trusted Logic (France), which is specialized in secure and
181 validated solutions for open systems, aims to present the
182 formalization and the demonstration of some security
183 properties related to the code embedded into a smart card. The presentation
184 must be in a format understandable by the company in charge of the
185 evaluation of the code and in accordance with the Common Criteria
187 <p>A third pilot application is the semantic markup of the Journal
188 <em>Living Reviews in Relativity</em> published by AEI-Golm,
189 already mentioned above.</p>