]> matita.cs.unibo.it Git - helm.git/blob - helm/mowgli/home/xml/consortium.xml
Markus Moschner (DFKI) added.
[helm.git] / helm / mowgli / home / xml / consortium.xml
1 <?xml version="1.0"?>
2
3 <!DOCTYPE consortium [
4  <!ELEMENT consortium (site+,description)>
5  <!ELEMENT site EMPTY>
6  <!ATTLIST site
7            file CDATA #REQUIRED>
8  <!ELEMENT description (p|dl|ul|ol)+>
9
10  <!-- A subset of XHTML -->
11  <!ELEMENT p (#PCDATA|em|a)*>
12  <!ELEMENT em (#PCDATA)>
13  <!ELEMENT a (#PCDATA)>
14  <!ATTLIST a
15            href CDATA #REQUIRED>
16  <!ELEMENT dl (dt|dd)+>
17  <!ELEMENT dt (#PCDATA)>
18  <!ELEMENT dd (#PCDATA)>
19  <!ELEMENT ul (li)+>
20  <!ELEMENT ol (li)+>
21  <!ELEMENT li (#PCDATA)>
22 ]>
23
24 <consortium>
25  <site file="bologna"/>
26  <site file="inria"/>
27  <site file="dfki"/>
28  <site file="nijmegen"/>
29  <site file="aei"/>
30  <site file="trusted-logic"/>
31  <description>
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>
35
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>
45   <dl>
46    <dt>MathML</dt>
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>
50
51    <dt>OpenMath</dt>
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>
56
57    <dt>OMDoc</dt>
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
61        issues.</dd>
62   </dl>
63
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,
67      as testified by the 
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>
74
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>
84
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>
100
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
112      and beyond.</p>
113
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>
134
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>
148
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
156      will agree to this.
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>
163
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>
179
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
186      standard.</p>
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>
190  </description>
191 </consortium>