X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmowgli%2Fhome%2Fxml%2Fconsortium.xml;fp=helm%2Fmowgli%2Fhome%2Fxml%2Fconsortium.xml;h=99cd1bea9d2527988e00783e244fa7b7397e8a6b;hb=d8ad1d26122af00feda930086b6cfa42de0139fe;hp=0000000000000000000000000000000000000000;hpb=05a794861b74ec8463dadf49492a22e078cc73f6;p=helm.git diff --git a/helm/mowgli/home/xml/consortium.xml b/helm/mowgli/home/xml/consortium.xml new file mode 100644 index 000000000..99cd1bea9 --- /dev/null +++ b/helm/mowgli/home/xml/consortium.xml @@ -0,0 +1,190 @@ + + + + + + + + + + + + + + + + + +]> + + + + + + + + + +

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.

+ +