| Monday
25. July | Tuesday
26. July | Wednesday
27. July | Thursday
28. July | Friday
29. July |
|---|
| 8:30 | Registration | Registration | Registration | Registration | Registration |
| Room | 2048 | 2001 | Aula | Aula | Aula | Aula | 2001 | Aula | 2048 |
| 9:00 | FM4M
Invited Talk: [F1]Chad Brown. Invited talk: Developments, Libraries and Automated Theorem Provers ( Slides)
Chair: Naumowicz | C. Sacerdoti
Coen
[I2]Claudio Sacerdoti Coen. Towards Extensible Algorithmic Mathematical Knowledge ( Slides)
Chair: Kohlhase | John Harrison
[I1]
Chair: Brown | Nicolas Thiery
[I3]Nicolas Thierry. Infrastructure for generic code in SageMath: categories, axioms, constructions ( Slides)
Chair: Sacerdoti Coen | | | |
| 10:00 | Coffee | Coffee | Coffee | Coffee | Coffee |
| 10:30 | Doctoral Program
[DP1]Marek Janasz. Automated theorem proving for elementary geometryDennis Müller. Knowledge Management across Formal LibrariesMoritz Schubotz. Augmenting Mathematical Formulae for More Effective Querying & Presentation ( Slides) Théo Zimmermann. Design and development of a tool based on Coq to write and format mathematical proofs
| MathUI
[M1]Lucius Schoenbaum. Towards Visual Type Theory as Mathematical Tool and Mathematical User InterfaceAndrea Kohlhase and Michael Fürsich. Understanding Mathematical Expressions: An Eye-Tracking Study
| FM4M
[F2]Adam Grabowski. Tarski's geometry and Euclidean plane in MizarMario Carneiro. Formalization of the prime number theorem and Dirichlet's theorem ( Slides) Karol Pąk. Topological Foundations for a Formal Theory of Manifolds
| MKM
[R5]Adam Naumowicz and Radosław Piliszek. Accessing the Mizar Library with a Weakly Strict Mizar ParserChad Brown and Josef Urban. Extracting Higher-Order Goals from the Mizar Mathematical Library ( Slides) Karol Pąk. Lemma Extraction Criteria Based on Properties of Theorem StatementsKarol Pąk and Aleksy Schubert. The impact of proof steps sequence on proof readability – experimental setting
Chair: Farmer
| Projects & Surveys
[R21]Paul-Olivier Dehaye, Mihnea Iancu, Michael Kohlhase, Alexander Konovalov, Samuel Lelièvre, Dennis Müller, Markus Pfeiffer, Florian Rabe, Nicolas M. Thiéry and Tom Wiesing. Interoperability in the OpenDreamKit Project: The Math-in-the-Middle ApproachWaqar Ahmed, Osman Hasan and Sofiene Tahar. Formal Dependability Modeling and Analysis: A Survey ( Slides)
Chair: Ion
| CALCULEMUS
[R4]Alexander Maletzky. Mathematical Theory Exploration in Theorema: Reduction RingsKen'Ichi Kuga, Manabu Hagiwara and Mitsuharu Yamamoto. Formalization of Bing's shrinking method in geometric topologyErika Ábrahám, Bernd Becker, James H. Davenport and Pascal Fontaine. SC-square: Satisfiability Checking meets Symbolic ComputationMuhammad Qasim, Osman Hasan, Maissa Elleuch and Sofiene Tahar. Formalization of Normal Random Variables in HOL ( Slides)
Chair: Naumowicz
| OpenMath | Mizar HandsOn Tutorial | MMT
Tutorial
|
| 11:30 | Systems & Data
[R18]Jan Jakubuv and Josef Urban. Extending E Prover with Similarity Based Clause Selection StrategiesArtur Kornilowicz. Enhancement of Mizar Texts with Transitivity Property of Predicates
Chair: Ion
|
| 12:30 | Lunch | Lunch | Lunch | Lunch | Lunch |
| 14:00 | OpenMath
Agenda, Standards Discussion
[O0]Michael Kohlhase. The 29th OpenMath Workshop, Agenda/PlanningTom Wiesing. An Overview over SCSCP | MathUI
[M3]Paul Libbrecht and Matija Lokar. The plain text trap when copying mathematical formulaeJuan Lao-Tebar, Francisco Alvaro and Daniel Marqus. Proposal for Coexistence of Mathematical Handwritten and Keyboard Input in a WYSIWYG Expression Editor
| FM4M/ThEdu
Invited Talk: [F6]Aleksy Schubert. Invited talk: On Differences in Proofs Between Intuitionistic and Classical LogicWalther Neuper. Lucas-Interpretation from Users’ Perspective ( Slides) | MKM
[R8]William Farmer. Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics ( Slides) Mario Carneiro. Models for Metamath ( Slides) Andreas Holmstrom. A first step towards automated conjecture-making in higher arithmetic geometry
Chair: Rabe
| Excursion | DML
[R32]Olaf Teschke and Fabian Müller. Progress of self-archiving within the DML corpus, with a view toward community dynamicsWolfram Sperber, Hagen Chrapary and Wolfgang Dalitz. swMATH - challenges, next steps, and outlook ( Slides) Hiroyuki Okazaki and Yuichi Futa. Formalization of Polynomially Bounded and Negligible Functions using the Computer-Aided Proof-Checking System Mizar
Chair: Davenport
| Tetrapod | Mizar HandsOn Tutorial |
| 15:30 | Coffee | Coffee | Coffee | Coffee |
| 16:00 | OpenMath
[O2]Bruce Miller. Drafting DLMF Content DictionariesMichael Kohlhase. Towards OpenMath 2.1 or 3; Issues and CriteriaMichael Kohlhase. Sequence Variables in OpenMath
| MathUI
[M5]Tom Wiesing and Felix Schmoll. KAT: an Annotation Tool for STEM DocumentsIon Toloaca and Michael Kohlhase. Notation-based Semantification
| FM4M/ThEdu
[T2]Walther Neuper. Rigor of TP in Educational Engineering Software ( Slides) Artur Korniłowicz. Registrations vs Redefinitions in MizarAdam Naumowicz. Linking to Compound Conditions in Mizar
| MKM
[W23]Thibault Gauthier, Cezary Kaliszyk and Josef Urban. Initial Experiments with Statistical Conjecturing over Large Formal CorporaCezary Kaliszyk, Michael Kohlhase, Dennis Müller and Florian Rabe. A Standard for Aligning Mathematical ConceptsDenis Rochau, Michael Kohlhase and Dennis Müller. FrameIT Reloaded: Serious Math Games from Modular Math Ontologies
Chair: Urban
| DML
[W45]Moritz Schubotz, David Veenhuis and Howard Cohl. Getting the units right ( Slides) Moritz Schubotz and Alan Sexton. A Smooth Transition to Modern mathoid-based Math Rendering in Wikipedia with Automatic Visual Regression Testing ( Slides)
Chair: Sorge
| Tetrapod | Mizar HandsOn Tutorial |
| 17:30 | General Meeting | | Track Meetings? | Business Meeting | |
| 19:00 | | Conference Dinner |
