| Monday
July 8 | Tuesday
July 9 | Wednesday
July 10 | Thursday
July 11 | Friday
July 12 |
|---|
| 9:00 | FMM1Chad Brown. Higher-Order Logic and Set Theory: Stronger Together | I1Makarius Wenzel. Interaction with Formal Mathematical Documents in Isabelle/PIDE
(chair: A. Kohlhase) | OM1Lars Hellström. Formalising Riemann Surfaces | LML1Makarius Wenzel. Isabelle technology for the Archive of Formal Proofs with application to MMT | I2Sylvain Corlay. Jupyter: From IPython to the Lingua Franca of Scientific Computing
(chair: C. Sacerdoti Coen) | I3Henry Prakken. AI models of argumentation and some applications to mathematics
(chair: C. Kaliszyk) |
| 9:30 | OM2Tom Wiesing. Proposed Standard Extension: A JSON Binding for OpenMath |
| 10:00 | Coffee | Coffee | Coffee | Coffee | Coffee |
| 10:30 | FMM2Adam Naumowicz. Testing Mizar User Interactivity in a University-level Introductory Course on Foundations of Mathematics | T9Alexander Maletzky. Formalization of Dubé's Degree Bounds for Gröbner Bases in Isabelle/HOL | chair: E. Brady | OM3Florian Rabe. Variables: Local Scope vs. Alpha-Renaming | LML2Claudio Sacerdoti Coen. Attempts at skinning an elephant | T10Chad Brown and Karol Pąk. A Tale of Two Set Theories | chair: M. Kohlhase | T14Tom Wiesing, Kai Amann, Michael Kohlhase and Florian Rabe. Integrating Semantic Mathematical Documents and Dynamic Notebooks | chair: J. Urban |
| 11:00 | FMM3Michael Junk and Stefan Hölle. Numerical MMATh | T16Jonas Bayer, Marco David, Abhik Pal and Benedikt Stock. Beginners' quest to formalize mathematics: A feasibility study in Isabelle | OM4Michael Kohlhase. OpenMath Society Business Meeting | LML3Wolfgang Dalitz, Wolfram Sperber, Moritz Schubotz, and Hagen Chrapary. alsoMATH - A Database for Mathematical Algorithms and Software | T12Abdou Youssef and Bruce Miller. Explorations into the Use of Word Embedding in Math Search and Math Semantics | T17Katja Berčič, Florian Rabe and Michael Kohlhase. Towards a Unified Mathematical Data Infrastructure: Database and Interface Generation |
| 11:30 | FMM4Peter Koepke. Textbook Mathematics in the Naproche-SAD System | T24Olaf Teschke, Vincent Stange, Moritz Schubotz, Norman Meuschke and Bela Gipp. Forms of Plagiarism in Digital Mathematical Libraries | LML4Gilles Dowek and François Thiré. Logipedia: a multi-system encyclopedia of formal proofs | T25Moa Johansson. Lemma Discovery for Induction - A survey | T18Florian Rabe. MMTTeX: Connecting Content and Narration-Oriented Document Formats |
| 12:00 | FMM5Artur Korniłowicz. Sethood Property in Mizar | DP1Sebastian Sahli. The MATh Tutor project | T52Besik Dundua, Temur Kutsia and Mircea Marin. Variadic Equational Matching | OM5Moritz Schubotz. Wiki Math Community Group Meeting | LML5Michael Kohlhase. The Data Aspect of Large Mathematical Libraries | Lunch | T32Florian Rabe and Yasmine Sharoda. Diagram Combinators in MMT |
| 12:30 | Lunch | Lunch | Lunch | Lunch |
| 13:30 | Excursion / Banquet |
| 14:00 | FMM6Adam Grabowski. Constructing Examples of Fuzzy Implications within the Mizar Mathematical Library | DP3Takuto Asakura. Understanding Scientific Documents with Synthetic Analysis on Mathematical Expressions and Natural Language | T34Matthew England and Dorian Florescu. Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition | chair: F. Rabe | WIP53Luis Berlioz. Creating a Database of Definitions From Large Mathematical Corpora | chair: A. Naumowicz | Tutorial: Exploring the MML |
| 14:30 | FMM7Adrian Jaszczak. Formal Verification of the Correctness of Chosen Algorithms in Mizar | DP4Joshua Chen. Hybrid and alternative logics in Isabelle | T11Zoltán Kovács and Pavel Pech. Experiments on automatic inclusion of some non-degeneracy conditions among the hypotheses in locus equation computations | WIP54Alexandre Bouquet and Thierry Bouche. GDML : Grenoble Digital Mathematics Library |
| 15:00 | FMM8Sofiene Tahar. Formalization of Dynamic Reliability Algebras in HOL | DP5Jonas Betzendahl. Definedness Reasoning in Formal Mathematics and Theorem Proving | T23Dee Quinlan, Joe Wells and Fairouz Kamareddine. BNF-Style Notation as it is Actually Used | WIP59Alexander Kirillovich, Olga Nevzorova, Marina Falileeva, Evgeny Lipachev and Liliana Shakirova. OntoMathEdu: Towards an Educational Mathematical Ontology |
| 15:30 | Coffee | Coffee | Coffee | Coffee |
| 16:00 | | DP6Max Rapp. A Unifying Framework for Managing Conflict-laden Content | T39William Farmer and Jacques Carette. Towards Specifying Symbolic Computation | chair: S. Tahar | T27Claudio Sacerdoti Coen. A Coq plugin to export its libraries to XML | chair: C. Brown | Tutorial: Exploring the MML |
| 16:30 | DP7Yasmine Sharoda. Leveraging Information Contained in a Theory Presentation | T29Andrea Condoluci, Michael Kohlhase, Dennis Müller, Florian Rabe, Claudio Sacerdoti Coen and Makarius Wenzel. Relational Data Across Mathematical Libraries | T49Dennis Müller, Florian Rabe and Claudio Sacerdoti Coen. The Coq Library as a Theory Graph |
| 17:00 | DP8Tom Wiesing. Evolving MathHub for Tetrapodal Math | T47Daniel Raggi, Aaron Stockdill, Mateja Jamnik, Grecia Garcia Garcia, Holly Sutherland and Peter Cheng. Inspection and selection of representations | Business Meeting
(chair: W. Farmer) |
| 17:30 | DP9Qingxiang Wang. Automating Formalization of Mathematics with Machine Learning and Data Mining | reception (18:00-20:00) |
| evening | |