Transcript PowerPoint - Interactive Mathematical Proof System

MoWGLI Mathematics in the Semantic Web
An Approach to Machine-Understandable
Representation of the Information in Digital Documents
Bernd Wegner
Technical University, Berlin
NA-MKM 2004, Phoenix, AZ
MoWGLI
Mathematics on the Web - Get it by Logic and
Interfaces
http://www.cs.unibo.it/mowgli
Funded by the 5. Framework Programme of the
EU
Start: March 2002
Duration: 3 years
Intermediate progress report in March 2003
successful
NA-MKM 2004
JMM pre-meeting, Phoenix January 2004
MoWGLI - objectives
Search and use mathematical content in the
web
Context related interpretation of formulas, links
to proof assistants
Content mark-up of electronic documents
Links between machine-readable and humanunderstandable presentation
NA-MKM 2004
JMM pre-meeting, Phoenix January 2004
MoWGLI - objectives
Exploitation of mark-up potentialities in
documents for
interoperability,
automation,
sophisticated search mechanisms,
intelligent applications
NA-MKM 2004
JMM pre-meeting, Phoenix January 2004
MoWGLI - partners
Department of Computer Science Bologna,
 project co-ordinator: Andrea Asperti
 HELM – Hypertextual Electronic Library of
Mathematics
 http://www.cs.unibo.it/helm
INRIA, Nice and Rocquencourt
Lemme -project for writing software in scientific
computing
LogiCal -Project (Coq proof assistant); common
features for proof checking and software security
NA-MKM 2004
JMM pre-meeting, Phoenix January 2004
MoWGLI - partners
German Research Centre for Artificial
Intelligence, DFKI, Saarbrücken/Kaiserslautern
ActiveMath - a web based learning environment
Relations to OmDoc and OpenMath
KU Nijmegen
automated theorem proving projects like
TYPES, FTA,
Calculemus,
OpenMath
NA-MKM 2004
JMM pre-meeting, Phoenix January 2004
MoWGLI - partners
Albert-Einstein-Institut (Max Planck Institute for
Gravitational Physics), Golm/Potsdam
Living Reviews in Relativity Theory
test bed for mark-up
development of LATEX-tools
Trusted Logic, France
Software quality and security aspects
Technical University Berlin (associated to AEI)
Exploitation and information dissemination
NA-MKM 2004
JMM pre-meeting, Phoenix January 2004
MoWGLI - initial actions
Requirement analysis - done
Investigations to determine the searchable
items in a document, development of metadata
schemes for their description - done
Preparation of the test bed “Living Reviews in
Relativity” - done, voluntary participation from
other “free” journals - postponed
Delivery of an exploitation and dissemination
plan - done
NA-MKM 2004
JMM pre-meeting, Phoenix January 2004
MoWGLI – general requirements
Tools should hook on developments from third
parties (open sources)
Authors should be able to apply them easily
No dependence from commercially protected
software
Possibilities for applications should be as wide
as possible
Chosen formats should be easily readable
NA-MKM 2004
JMM pre-meeting, Phoenix January 2004
MoWGLI – problems and solutions
Application of XML-technology is standard
DFKI and Nijmegen/Eindhoven use OpenMath
and OmDoc for the encoding of mathematical
objects
DFKI has created an OmDoc based
mathematical database
Presentation done by HTML/MathML
MathML is supported by the main webbrowsers: Mozilla, Netscape, Internet-explorer
NA-MKM 2004
JMM pre-meeting, Phoenix January 2004
MoWGLI – problems and solutions
Scheme of translations:
XML to OmDoc, OmDoc to HTML/MathML via
presentation XSLT
http://www.w3.org/TR/xslt
Conversion from Coq to OmDoc available
Interactive course notes from Eindhoven, which
are textual mathematical documents, enhanced
with the possibility to interact with a computer
algebra system through OpenMath objects
NA-MKM 2004
JMM pre-meeting, Phoenix January 2004
MoWGLI – problems and solutions
Representation and selection problems
MathML can be produced using appropriate
editors only
Selection schemes for content mark-up have to
be developed
The same for formulas
Unique and coordinated search facilities for
formulas are required (different TEX-codings)
NA-MKM 2004
JMM pre-meeting, Phoenix January 2004
MoWGLI – problems and solutions
Proof assistants have to deal with two versions:
machine understandable vs.
human understandable
INRIA (Nice) provides applications (and
conversions) for applying Coq to proofs in
elementary geometry and incidence geometry
(using TexMacs)
AEI has delivered a LaTeX conversion to
presentation MathML
NA-MKM 2004
JMM pre-meeting, Phoenix January 2004
MoWGLI – problems and solutions
Possibly TEX- and MathML extensions are
requested to comply with further requirements
First release for metadata schemes is available
and compliant with other systems like OAI,
EULER etc.
An alternative approach to some problems is
provided by MAYA from DFKI (with strong
relations to OmDoc)
OmDoc content dictionaries are available
NA-MKM 2004
JMM pre-meeting, Phoenix January 2004
MoWGLI – open ends
Controlled vocabulary still is missing, but
essential for further progress
Nothing has been and could be done with
respect to graphics within the project. This is
beyond the expertise of most of the partners in
the current group.
As far as presentation will be concerned the
project will be able to deliver good results.
Development of interactive input components
will be beyond the capacity of the current
project.
NA-MKM 2004
JMM pre-meeting, Phoenix January 2004
MoWGLI –
relations to the mathematical community
Project is pursued by experts in knowledge
management and artificial intelligence
Comments from mathematicians are needed
concerning
Relevance of the ideas for mathematical publications
Background information for semantic mark-up
(names, notions, identification, keywords, etc.)
User-friendliness of the developed tools
Extension of the test bed “Living Reviews in
Relativity” is highly desirable.
NA-MKM 2004
JMM pre-meeting, Phoenix January 2004
Adresses
Bernd Wegner
Mathematisches Institut, TU Berlin, Sekr. MA 8-1
Straße des 17. Juni 135, D-10623 Berlin
E-Mail
[email protected]
http://www.cs.unibo.it/mowgli
http://www.emis.de
NA-MKM 2004
JMM pre-meeting, Phoenix January 2004