X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fmowgli%2Fhome%2Fxml%2Fconsortium.xml;fp=helm%2Fmowgli%2Fhome%2Fxml%2Fconsortium.xml;h=0000000000000000000000000000000000000000;hp=c21af1537e1c8b253a0eeca345f3207d5b676626;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1 diff --git a/helm/mowgli/home/xml/consortium.xml b/helm/mowgli/home/xml/consortium.xml deleted file mode 100644 index c21af1537..000000000 --- a/helm/mowgli/home/xml/consortium.xml +++ /dev/null @@ -1,191 +0,0 @@ - - - - - - - - - - - - - - - - - - -]> - - - - - - - - - -

The Consortium has been built with the aim to join some essential - knowhow in different areas of I.T. related to the creation and - maintenance of a digital library of structured mathematical knowledge.

- -

MOWGLI is meant to develop the technological infrastructure required to - integrate existing Markup languages and standards such as - MathML, - OpenMath or - OMDoc, - covering different aspects of mathematical - intelligence, into a single application. - Expertise on these languages and the related technologies is - respectively provided by the following partners:

-
-
MathML
-
Department of Computer Science, University of Bologna, - member of the World Wide Web Consortium and of the W3C Working Group - on MathML; Lemme-Project at INRIA Sophia-Antipolis.
- -
OpenMath
-
University of Eindhoven (sub-site of Nijmegen): - Professor Arjeh Cohen is one of the leaders of the - OpenMath initiative, and MOWGLI is expected to take the maximum profit - from the successful OpenMath Esprit project, no.24969.
- -
OMDoc
-
DFKI. Dr.Michael Kohlhase is the main - auhtor of OMDoc; DFKI has a long research tradition in the management of - mathematical knowledge bases, metadata, searching and retrieval - issues.
-
- -

More generally, the Department of Computer Science in Bologna has a - long experience in XML-related technology, and in particular in their - application to the particular domain of mathematical developments, - as testified by the - ``Hypertextual Electronic Library - of Mathematics'' (HELM) Project. A main - component of HELM is the - GtkMathView - widget, a C++ rendering engine for MathML that will be distributed as - an official package of the next Debian release of Linux.

- -

Similarly, the Lemme Project in Sophia-Antipolis has a large experience of - edition of mathematical objects. It develops the graphical environment - Pcoq, dedicated to the development of mathematical proofs, using the - Coq proof assistant. Among many features, Pcoq has a sophisticated two - dimensional formula and natural language proof edition component, - allowing intuitive and powerful interactions. Built on the Figue - environment, Pcoq can be made compatible with MathML. The Pcoq interface - is intensively used by teams whose research activity concerns - the certification of mathematical algorithms.

- -

DFKI will contribute requirements and metadata from the - viewpoint of educational applications including search - functionalities. It will actively work on presentational transformations, - the generation of proofs in natural language as well as on knowledge bases - for mathematical knowledge DFKI intends to exploit the results of the - MOWGLI project in pilot applications in current and planned research and - in projects for the prototypical implementation of intelligent - environments for learning of mathematics. In particular, the knowledge - representation for mathematics on the Web is important for such Web-based - systems. Knowledge bases that provide a common repository and ontology for - mathematical knowledge are indispensible in systems that integrate various - systems working on mathematical knowledge. DFKI also has a fierce interest - in pushing and leveraging the quality of standardisation efforts within - the worldwide initiative of the Semantic Web education systems and - electronic publishing.

- -

In order to immediately dispose of a large repository of structured - mathematical information, the consortium comprises the developers of - one of the most successful proof assistant tools currently - available: the Coq proof - engine of INRIA-Rocquencourt. - The Coq standard library includes more than thousand lemmas and theorems - and the whole number of statements proved by users is evaluated to - hundred thousands, covering arithmetics, algebra, analysis and - computer science. We expect to integrate the current different ways of - browsing, searching and rendering Coq mathematical developments into a - coherent and Web-oriented architecture open to the Coq user community - and beyond.

- -

An alternative route for the creation of content-based mathematical - information from standard digital repositories by means of a suitable - LaTeX-based authoring system will be explored by the Albert - Einstein Institute (AEI) in Golm (Germany). AEI publishes a solely - electronic review journal, Living Reviews in Relativity on - the Web, which provides refereed, regularly updated review - articles on all areas of gravitational physics. Since its - release in January 1998 the journal has become a primary - entry point for students, lecturers and researchers alike - for up-to-date information on the current status of research - in gravitational physics. Moving this unique repository and - communication forum of current physical and mathematical - knowledge in relativity to content mark-up, making it - available for semantic search, and for re-use and evaluation - e.g. in math algebra systems motivates the involvement - in the MOWGLI project. The journal will develop a - LaTeX based authoring tool interfacing with MOWGLI, and - serve as a showcase to demonstrate how content-mark-up in - mathematics improves the usability and information depth - of electronic science journals.

- -

The AEI will be supported by the newly founded Center for Information - Management (CIM) of the Max Planck Society. The CIM has been set up - by the Society to support researchers and research processes in the area - of information management. The objectives of the project include - coordination of existing activities within the Society and - implementation of a strategy to develop electronic research archives. - The current Managing Editor of the AEI's electronic journal Living - Reviews in Relativity has been appointed executive director of the CIM - (starting from 1 Sep 2001) and will be in charge of the project management - for Tasks 4.4 and 6.3 of the proposal. The CIM will be in an - excellent position to promote dissemination and use of the project results - within the Max Planck Society. It will further give technical support to - the Dissemination Manager in providing the MOWGLI website.

- -

Professor Wegner, Scientific Coordinator of EMIS (European - Mathematical Information Service), will also provide a main liaison with - previous and successful European Projects on digital libraries and - metadata, such as EULER - and the TRIAL Solution project (\verb+http://www.trial-solution.de+). - In particular, all the achievements of these Projects - will be integrated inside MOWGLI, as far as the respective teams - will agree to this. - Moreover, in his quality of Scientific Coordinator of EMIS, member - of the advisory board for MATHDI, and Chairman of the Electronic - Publishing Committee of European - Mathematical Society, Professor Wegner is an excellent candidate - to organise the information - dissemination and exploitation activities for the project.

- -

In particular, the Department of Computer Science of the University of - Nijmegen will apply MOWGLI's technologies to the development of - an ``electronic book'', covering a typical undergraduate course - in Algebra or Analysis. The Department of Computer Science in Nijmegen - has a lot of experience in formal mathematics and theorem proving. - Notably, the group has done large theory developments in the theorem - prover Coq. (The FTA - project: Eindhoven University of Technology, a sub-site of Nijmegen, - has expertise in OpenMath and in using WWW technology for educational - purposes. This has resulted -- among other things -- in - IDA, the - interactive course notes in algebra where a combination of HTML - and applets is used to present the mathematics. Jointly, Nijmegen and - Eindhoven have experience in combining theorem provers and computer - algebra packages, notably Coq and GAP.

- -

Trusted Logic (France), which is specialized in secure and - validated solutions for open systems, aims to present the - formalization and the demonstration of some security - properties related to the code embedded into a smart card. The presentation - must be in a format understandable by the company in charge of the - evaluation of the code and in accordance with the Common Criteria - standard.

-

A third pilot application is the semantic markup of the Journal - Living Reviews in Relativity published by AEI-Golm, - already mentioned above.

- -