BEGIN:VCALENDAR VERSION:2.0 PRODID:-//Talks.cam//talks.cam.ac.uk// X-WR-CALNAME:Talks.cam BEGIN:VEVENT SUMMARY:Lightweight and Heavyweight Methods for Integrating Mathematical L ibraries - Michael Kohlhase (Jacobs University Bremen) DTSTART:20170714T090000Z DTEND:20170714T100000Z UID:TALK73277@talks.cam.ac.uk CONTACT:INI IT DESCRIPTION:Arguably\, the most crucial resource for scaling up math ematical proof to
the Internet age is the availability of machine-acti onable libraries of
mathematical knowledge as well as information syst ems and semantic
services based on these libraries.

There are various mathematical knowledge collections and information
systems av ailable. They range from completely informal ones like
Wikipedia or th e Cornell arXiv\, zbMath\, and MathSciNet via mathematical
object data bases like the GAP group libraries\, the Online Encyclopedia
of Intege r sequences (OEIS)\, and the L-functions and Modular Forms
Database (L MFDB) to theorem prover libraires like those of Mizar\, Coq\,
PVS\, an d the HOL systems.

Unfortunately\, while all of these individuall y constitute steps into the
direction of research data\, they attack t he problem at different levels
(object\, vs. document level) and direc tion (description- vs.
classification-based) and are mutually incompat ible and
not-interlinked/aligned systematically.

I will surve y methods and systems which can act as stepping stones
towards unifyin g these seeds into a Global Digital Library of
Mathematics. These meth ods and systems are inherently of flexible
formality (flexiformal) and range from heavyweight methods like
developing modular meta-logical f ormats for co-representing logics and
libraries in a common global mea ning-space via all kinds of library
translations to lightweight method s for aligning and cross-linking such
libraries.

I will exemp lify the methods on pragmatic examples (e.g. translating
LaTeX to HTML 5 for arXiv.org< /a> importing PVS to OMDoc/MMT\, or parsing the
OEIS) and discuss the infrastructures we need for managing a global\,
flexiformal digital ma thematical mathematical library. LOCATION:Seminar Room 1\, Newton Institute END:VEVENT END:VCALENDAR