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