Schedule per day| Monday | |
| 8:00 - 9:00 | Registration | | 9:00 - 10:00 | Mathematical Knowledge ManagementChair: Josef Urban, Room (amphitheatre) Pedro Nunes (1st floor)
| OpenMath WorkshopRoom (amphitheatre) 2.4 (2nd floor)
| | 10:00 - 10:30 | Coffee | | 10:30 - 12:30 | Mathematical Knowledge ManagementChair: Freek Wiedijk/Stephen Watt, Room (amphitheatre) Pedro Nunes (1st floor)
| OpenMath WorkshopRoom (amphitheatre) 2.4 (2nd floor)
| | 12:30 - 14:30 | Lunch | | 14:30 - 16:00 | Mathematical Knowledge ManagementChair: Cezary Kaliszyk, Room (amphitheatre) Pedro Nunes (1st floor)
| OpenMath WorkshopRoom (amphitheatre) 2.4 (2nd floor)
- OpenMath Business Meeting, discussion of proposals (14:30-16:00)
| | 16:00 - 16:30 | Coffee | | 16:30 - 18:00 | Work-in-ProgressChair: Stephen Watt, Room (amphitheatre) Pedro Nunes (1st floor)
| Doctoral ProgrammeChair: David Wilson, Room (amphitheatre) 2.4 (2nd floor)
- Ieuan Evans. Mathematical Document Classification via the Pachinko Allocation Model (16:30-17:00)
- Washington Segundo. Formalizing a named calculus modulo alpha-equivalence (17:00-17:30)
- Denise Torrão. Algebraic Algorithms for Numerical Semigroups (17:30-18:00)
| | 20:00 - | | |
| Tuesday | |
| 8:00 - 9:00 | | | 9:00 - 10:00 | Mathematical Knowledge ManagementChair: Florian Rabe, Room (amphitheatre) Pedro Nunes (1st floor)
| Notion of ProofRoom (amphitheatre) 2.4 (2nd floor)
- Michael Kinyon. Quasigroups, Loops and Automated Deduction, or How I Learned To Stop Worrying and Start Letting Computers Prove Theorems (9:00-9:40)
- Ursula Martin. Is mathematics a social machine? (9:40-10:00)
| | 10:00 - 10:30 | Coffee | | 10:30 - 12:30 | CalculemusChair: Florian Rabe/Alan Sexton, Room (amphitheatre) Pedro Nunes (1st floor)
Cylindrical Algebraic Decomposition
- Russell Bradford, Changbo Chen, James H. Davenport, Matthew England, Marc Moreno Maza and David Wilson. Problem formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition (10:30-11:00) (Slides) (DOI)
- Zongyan Huang, Matthew England, David Wilson, James Davenport, Lawrence Paulson and James Bridge. Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition (11:00-11:30) (Slides) (DOI)
- (Invited Talk) Eric Weisstein. Computable data, mathematics, and digital libraries in Mathematica and Wolfram|Alpha (11:30-12:30) (DOI)
| Notion of ProofRoom (amphitheatre) 2.4 (2nd floor)
- Freek Wiedijk. Extreme mathematics (10:30-11:10)
- Jamie Gaspar. Short introduction by example to Coq (11:10-11:30)
| | 12:30 - 14:30 | Lunch | | 14:30 - 16:00 | CalculemusChair: James Davenport, Room (amphitheatre) Pedro Nunes (1st floor)
Novel Applications
| Notion of ProofRoom (amphitheatre) 2.4 (2nd floor)
- Arie Hinkis. The representation of mathematical proof through gestalt and metaphors (14:30-14:50)
- Mark Adams. Proof Auditing for Formalised Mathematics (14:50-15:10)
- William Farmer. Can Computer Proving Replace Traditional Proving? (15:10-15:30)
| | 16:00 - 16:30 | Coffee | | 16:30 - 18:00 | Room (amphitheatre) Pedro Nunes (1st floor)
| | | 20:00 - | | |
| Wednesday | |
| 8:00 - 9:00 | | | 9:00 - 10:30 | Mathematical Knowledge ManagementChair: Stephen Watt, Room (amphitheatre) Pedro Nunes (1st floor)
| Theorem Provers Components for Educational SoftwareRoom (amphitheatre) 2.4 (2nd floor)
| | 10:30 - 11:00 | Coffee | | 11:00 - 12:30 | CalculemusChair: Matthew England, Room (amphitheatre) Pedro Nunes (1st floor)
Theories
| Theorem Provers Components for Educational SoftwareRoom (amphitheatre) 2.4 (2nd floor)
| | 12:30 - 14:30 | Lunch | | 14:30 - 16:30 | Chair: Carlota Simões, Amphitheatre of the Science Museum (Laboratorio Chimico)
- (Invited Talk) António Leal Duarte. Teaching Tiles (joint with ADG 2014) (14:30-15:30)
- Visit of Science Museum & Port Wine tasting (15:30 - 16:30)
| | | 16:30 - 18:00 | - Visit U. Coimbra (16:30 - 18:00)
- Walk downtown (18:00 - 19:00)
| | | 20:00 - | - Gala Dinner (20:00 - 23:00)
| |
| Thursday | |
| 8:00 - 9:00 | | | 9:00 - 10:00 | Work-in-ProgressChair: James Davenport, Room (amphitheatre) Pedro Nunes (1st floor)
| Mathematical User InterfacesRoom (amphitheatre) 2.4 (2nd floor)
| | 10:00 - 10:30 | Coffee | | 10:30 - 12:30 | Doctoral ProgrammeChair: David Wilson/James Davenport, Room (amphitheatre) Pedro Nunes (1st floor)
| Mathematical User InterfacesRoom (amphitheatre) 2.4 (2nd floor)
| | 12:30 - 14:30 | Lunch | | 14:30 - 16:00 | Systems & ProjectsChair: Alan Sexton, Room (amphitheatre) Pedro Nunes (1st floor)
Teaser Talks
- 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)
| Mathematical User InterfacesRoom (amphitheatre) 2.4 (2nd floor)
| | 16:00 - 16:30 | Coffee | | 16:30 - 18:00 | 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)
| Mathematical User InterfacesRoom (amphitheatre) 2.4 (2nd floor)
| | 20:00 - | | |
| 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 - | | | |
|
