The consortium was formed following the First
Conference On Mathematical Knowledge Management, held in September 2001 at
RISC. It is a broad-based consortium, largely but not exclusively academic,
aimed at covering the range of mathematical knowledge from the totally formal,
through the rigorous but informal language of the mathematical literature, to
the mathematics appearing in the documentation of software. Equally, it covers
many different fields of mathematics (Number Theory, Cryptography, Logic,
Numerical Analysis and many others).
The University of Bath
The University of Bath
is the project coordinator. The University's
Department
of Computer Science
has been involved in EU-funded projects since 1986, has
coordinated several, and will be
using an experienced academic, Prof. Davenport, as Project Manager, assisted by
the project management assistant on previous EU-funded projects run from the
University of Bath. In Prof. Davenport, the University of Bath provides
the Editor-in-Chief of the London Mathematical Society's Journal of Computation
and Mathematics: a fully refereed electronic journal, with a full-text search
engine. This technology is far from perfect, since the user would like a
formula-based capability in the search engine.
The Numerical Algorithms Group (NAG)
The Numerical Algorithms Group
is Europe's largest vendor of mathematical software. NAG is
fundamentally a provider of mathematical algorithms through its
numerical libraries and other products. The most recent release of
its Fortran-77 Library (mark 20) contains 1250 user-level routines,
each of which is documented in both printed and online forms. The
printed documentation is over 70cm thick while the online version
consists of over 400Mb of PDF files. Allowing better organisation
and navigation of this information would be of direct benefit to
both NAG and its user's, and this has motivated the Company to
become involved in both the
OpenMath project (where it was the
coordinating partner) and the W3C
Math Working Group. NAG is
committed to the development of open standards and has an extensive
track-record in this area (Fortran-90, Java Grande, Basic Linear
Algebra Subset etc.).
University College London
University College London
has a large and flourishing computer science department. One of the
department's specialities is human-computer interaction.
Specifically, the needs of mathematicians will be addressed by
taking a user-centred approach to developing mathematical knowledge
management techniques. And conversely, good tools for
mathematicians will not come without good mathematical knowledge
management underlying those tools.
Heriot-Watt University
Heriot-Watt University
has considerable strength in research on logics, types, rewriting,
their automation and application to programming languages, theorem
proving, and mathematics. This research has been supported by
considerable funding (EU/EC, EPSRC, NWO (Dutch research council),
Royal Society, NSF(USA), etc.) and has resulted in seven
international workshops/schools at Heriot-Watt in the past 3 years
on themes related to this network.
The University of Birmingham
The computer science department at the University of Birmingham has
a wide range of research activities in the fields of automated
reasoning, theorem proving and knowledge representation. There are
relevant interests in databases and the development of complex
index structures to adequately store and retrieve mathematical
knowledge.
Université Pierre et Marie (Paris 6)
Université Pierre et Marie (Paris 6)
has relevant research interests in type theory (unification,
deduction modulo), semantics and formal methods for critical code.
The research project FOC develops an environment for certified
computer algebra. Starting with a source in FOC both an executable
procedure (in Objective CAML) and skeletons of proofs of the
correctness of these procedures, may be derived. These skeleton
proofs are then automatically or interactively completed and
checked using the theorem prover Coq.
CWI
CWI is the major Dutch centre for research in computer science. As a
descendant of the Mathematisch Centrum, it has always had a strong
interest in the relationships between mathematics and computer
science last 10 years on a variety of matters concerning
mathematical knowledge, especially metadata, indexes and thesauri.
German Research Center for Artificial Intelligence (DFKI)
The German Research Center for Artificial Intelligence GmbH, (DFKI)
with sites in Kaiserslautern and Saarbrücken is the leading
German research institute in the field of innovative software
technology. In the international scientific community, the DFKI is
among the important ``Centers of Excellence''. Prof. Jörg
Siekmann's research group concentrates on multi-agent systems,
program verification and software security, and computer-supported
education.
Saarland University (USAAR)
The Institute of Computer Science of Saarlandes constitute a famous
center for research in representing, proving (creating) and
processing mathematical knowledge. The
OMEGA group has studied
automated theorem proving, knowledge-based proof planning , and
mathematical knowledge representation for over 20 years. The
OMEGA project
is part of the the collaborative research centre of
Resource-adaptive Cognitive Processes (SFB 378), and has
strong ties with the DFKI group and the Max-Planck Institute for
Computer Science in Saarbrücken.
RISC
The Research Institute for Symbolic Computation is an institute of
the University of Linz, Austria. RISC is dedicated to excellence in
teaching, research, and applications of symbolic computation,
notably computer algebra and automated reasoning. In particular,
since 1994, the research group under the leadership of Prof. Bruno
Buchberger is developing the Theorema system based on Mathematica,
which aims to automate in an unified framework the main activities
of the working mathematician: proving, computing, and solving. RISC
and SCCH organized in 2001 the first international workshop on
mathematical knowledge management.
The Software Competence Center Hagenberg (SCCH)
The Software Competence Center Hagenberg
is a company that was founded by five institutes of the University
of Linz as academic partners and fifteen companies as industrial
partners to cooperated in application-oriented research projects in
the areas Software Technology, Data Base Technology, Knowledge
Based Technology, Symbolic and Numerical Computation.
Bologna
The Department of Computer Science of Bologna is the only
educational institution in Italy to be affiliated to the World Wide
Web Consortium (and one of the few members of this category in
Europe). This affiliation testifies the interest, both technical
and didactic, traditionally devoted by our Department to Web
technologies, Internet and, more generally, distributed computing.
It is home of the highly relevant
HELM project
Universität Koblenz-Landau.
The Computer Science Department at the University of Koblenz-Landau
comprises 23 professorships. Teaching and research in the Computer
Science Department covers both core and applied disciplines. The
Artificial Intelligence Research Group, led by Prof. Dr. Ulrich
Furbach, is pursuing internationally acknowledged research in
various AI disciplines. Of particular relevance for the project is
the expertise in Knowledge Representation, Automated Deduction
Systems and E-learning technology.
Bialystok
For over two decades the Mizar Group at the University of Bialystok
has been developing a computer proof checking system with input
language close to a mathematical vernacular. Mizar system
provides an environment in which mathematical texts written in the
Mizar language are checked for correctness. This is a long term
project aiming at building a comprehensive library of mathematical
knowledge. As of February 2002, Mizar Mathematical Library consists
of 709 articles (50 MB, 32 000 theorems and 7000 definitions). The
journal of Formalized Mathematics of Mizar articles has been
published since 1990, now
on the web; truly
oriented to effectively use the capabilities of the electronic
medium, including extensive cross-referencing practical only in
such an environment.