]> matita.cs.unibo.it Git - helm.git/blob - helm/mowgli/home/xml/consortium.xml
Initial commit of the XML/XSLT stuff.
[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)+>
9
10  <!-- A subset of XHTML -->
11  <!ELEMENT p (#PCDATA|I|a)*>
12  <!ELEMENT I (#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 li (#PCDATA)>
21 ]>
22
23 <consortium>
24  <site file="bologna"/>
25  <site file="inria"/>
26  <site file="dfki"/>
27  <site file="nijmegen"/>
28  <site file="aei"/>
29  <site file="trusted-logic"/>
30  <description>
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>
34
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>
44   <dl>
45    <dt>MathML</dt>
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>
49
50    <dt>OpenMath</dt>
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>
55
56    <dt>OMDoc</dt>
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
60        issues.</dd>
61   </dl>
62
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,
66      as testified by the 
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>
73
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>
83
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>
99
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
111      and beyond.</p>
112
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>
133
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>
147
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
155      will agree to this.
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>
162
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>
178
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
185      standard.</p>
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>
189  </description>
190 </consortium>