ocaml 3.09 transition

[helm.git] / helm / mowgli / home / xml / consortium.xml

<?xml version="1.0"?>

<!DOCTYPE consortium [
 <!ELEMENT consortium (site+,description)>
 <!ELEMENT site EMPTY>
 <!ATTLIST site
           file CDATA #REQUIRED>
 <!ELEMENT description (p|dl|ul|ol)+>

 <!-- A subset of XHTML -->
 <!ELEMENT p (#PCDATA|em|a)*>
 <!ELEMENT em (#PCDATA)>
 <!ELEMENT a (#PCDATA)>
 <!ATTLIST a
           href CDATA #REQUIRED>
 <!ELEMENT dl (dt|dd)+>
 <!ELEMENT dt (#PCDATA)>
 <!ELEMENT dd (#PCDATA)>
 <!ELEMENT ul (li)+>
 <!ELEMENT ol (li)+>
 <!ELEMENT li (#PCDATA)>
]>

<consortium>
 <site file="bologna"/>
 <site file="inria"/>
 <site file="dfki"/>
 <site file="nijmegen"/>
 <site file="aei"/>
 <site file="trusted-logic"/>
 <description>
  <p>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.</p>

  <p>MOWGLI is meant to develop the technological infrastructure required to
     integrate existing Markup languages and standards such as
     <a href="http://www.w3.org/Math/">MathML</a>,
     <a href="http://www.openmath.org">OpenMath</a> or
     <a href="http://www.mathweb.org/omdoc/">OMDoc</a>,
     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:</p>
  <dl>
   <dt>MathML</dt>
   <dd>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.</dd>

   <dt>OpenMath</dt>
   <dd>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.</dd>

   <dt>OMDoc</dt>
   <dd>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.</dd>
  </dl>

  <p>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 
     <a href="http://www.cs.unibo.it/helm">``Hypertextual Electronic Library
     of Mathematics'' (HELM) Project</a>. A main
     component of HELM is the
     <a href="http://www.cs.unibo.it/helm/mml-widget/index.html">GtkMathView
     widget</a>, a C++ rendering engine for MathML that will be distributed as
     an official package of the next Debian release of Linux.</p>

  <p>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.</p>

  <p>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.</p>

  <p>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 <a href="http://pauillac.inria.fr/coq/">Coq</a> 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.</p>

  <p>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, <em>Living Reviews in Relativity</em> 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.</p>

  <p>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.</p>

  <p>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 <a href="http://www.emis.de/projects/EULER">EULER</a>
     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.</p>

  <p>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 <a href="http://www.cs.kun.nl/gi/projects/fta/">FTA
     project</a>: 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
     <a href="http://www.win.tue.nl/~ida/">IDA</a>, 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.</p>

  <p>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.</p>
  <p>A third pilot application is the semantic markup of the Journal
     <em>Living Reviews in Relativity</em> published by AEI-Golm,
     already mentioned above.</p>
 </description>
</consortium>