Day Programme Friday| Friday | |
| 8:00 - 9:00 | | | 9:00 - 10:00 | Digital Mathematical LibrariesChair: Bernd Wegner, Room (amphitheatre) Pedro Nunes (1st floor)
| Doctoral ProgrammeChair: David Wilson, Room (amphitheatre) 2.4 (2nd floor)
- Waqar Ahmed. Formal Analysis of Reliability Block Diagrams (9:00-9:30)
- Umair Siddique. Formal Analysis of Geometrical Optics in HOL (9:30-10:00)
| | | 10:00 - 10:30 | Coffee | | 10:30 - 12:30 | Digital Mathematical LibrariesChair: Petr Sojka, Room (amphitheatre) Pedro Nunes (1st floor)
| Doctoral ProgrammeChair: David Wilson, Room (amphitheatre) 2.4 (2nd floor)
- Zongyan Huang. Machine learning and computer algebra (10:30-11:00)
- Burak Ekici. Certification of programs with computational effects (11:00-11:30)
| | | 12:30 - 14:30 | Lunch | | 14:30 - 15:30 | Digital Mathematical LibrariesChair: Alan Sexton, Room (amphitheatre) Pedro Nunes (1st floor)
- tentative list of panelists: Fabian Müller (FIZ/ZMath), Michael Kohlhase (Jacobs), [Herbert Van de Sompel (LANL)], Eric Weisstein (Wolfram|Aplha), Petr Sojka (Masaryk University). DML panel discussion: DMLs of Informal and Formal Mathematics: Marriage or Divorce? (14:30 -- 15:30)
Abstract:
There are two areas/worlds/directions where term DML
(Digital Mathematics Libraries) is used:
a) library of [informal] scientific [mostly peer-reviewed]
papers that are have been written in the area of
mathematics since Aristotle. Most papers in this
world have been digitized and persistent pointers
(DOIs, Zbl or MathSciNet IDs) are used as pointers
to them. This allowed to build a web of linked and
verified (reviews in referative databases) mathematical
knowledge. In CICM jargon, DML track copes with this area
and Herbert Van de Sompel's talk dealt with
problems of linking and persistence in this world.
b) library of [formal] mathematics knowledge, e.g.
theorems formally proven by systems as Wolfram|Alpha,
Coq, Mizar and others. Libraries of such math
knowledge are poping up.
In CICM jargon, MKM track copes with this area
and Eric Weisstein's invited talk (eCF library)
elaborated on current possibilities in this world.
| | | | 15:30 - 16:00 | Coffee | | 16:00 - 18:00 | Digital Mathematical LibrariesChair: Michael Kohlhase, Room (amphitheatre) Pedro Nunes (1st floor)
| Work-in-ProgressChair: Andrea Kohlhase, Room (amphitheatre) Pedro Nunes (1st floor)
| Systems & ProjectsRoom 0.2 (0th floor)
Demos
- Howard Cohl, Marjorie McClain, Bonita Saunders, Moritz Schubotz and Janelle Williams. Digital Repository of Mathematical Formulae (16:30-18:00, Thursday 14:30-15:30, Thursday 16:00-18:00) (DOI)
- Deyan Ginev and Joseph Corneli. NNexus Reloaded (16:30-18:00, Thursday 14:30-15:30, Thursday 16:00-18:00) (DOI)
- Deyan Ginev, Bruce Miller and Silviu Oprea. E-books and Graphics with LaTeXML (16:30-18:00, Thursday 14:30-15:30, Thursday 16:00-18:00) (DOI)
- Mihnea Iancu, Constantin Jucovschi, Michael Kohlhase and Tom Wiesing. System Description: MathHub.info (16:30-18:00, Thursday 14:30-15:30, Thursday 16:00-18:00) (DOI)
- Cezary Kaliszyk, Josef Urban, Jiří Vyskočil and Herman Geuvers. Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description (16:30-18:00, Thursday 14:30-15:30, Thursday 16:00-18:00) (DOI)
- Lukas Kohlhase and Michael Kohlhase. System Description: A Semantics-Aware LaTeX-to-Office Converter (16:30-18:00, Thursday 14:30-15:30, Thursday 16:00-18:00) (DOI)
- Martin Líška, Petr Sojka and Michal Růžička. Math Indexer and Searcher Web Interface: Towards Fulfillment of Mathematiciansí Information Needs (16:30-18:00, Thursday 14:30-15:30, Thursday 16:00-18:00) (Slides) (DOI)
- Adam Naumowicz. SAT-enhanced Mizar Proof Checking (16:30-18:00, Thursday 14:30-15:30, Thursday 16:00-18:00) (DOI)
- Umair Siddique and Sofiene Tahar. A Framework for Formal Reasoning about Geometrical Optics (16:30-18:00, Thursday 14:30-15:30, Thursday 16:00-18:00) (DOI)
| | 20:00 - | | | |
|
