List of Events

Invited Talks

• [I1] Makarius Wenzel. Interaction with Formal Mathematical Documents in Isabelle/PIDE
• [I2] Sylvain Corlay. Jupyter: From IPython to the Lingua Franca of Scientific Computing
• [I3] Henry Prakken. AI models of argumentation and some applications to mathematics

Full Paper Presentations

• [T9] Alexander Maletzky. Formalization of Dubé's Degree Bounds for Gröbner Bases in Isabelle/HOL
• [T10] Chad Brown and Karol Pąk. A Tale of Two Set Theories
• [T11] Zoltán Kovács and Pavel Pech. Experiments on automatic inclusion of some non-degeneracy conditions among the hypotheses in locus equation computations
• [T12] Abdou Youssef and Bruce Miller. Explorations into the Use of Word Embedding in Math Search and Math Semantics
• [T14] Tom Wiesing, Kai Amann, Michael Kohlhase and Florian Rabe. Integrating Semantic Mathematical Documents and Dynamic Notebooks
• [T16] Jonas Bayer, Marco David, Abhik Pal and Benedikt Stock. Beginners' quest to formalize mathematics: A feasibility study in Isabelle
• [T17] Katja Berčič, Florian Rabe and Michael Kohlhase. Towards a Unified Mathematical Data Infrastructure: Database and Interface Generation
• [T18] Florian Rabe. MMTTeX: Connecting Content and Narration-Oriented Document Formats
• [T23] Dee Quinlan, Joe Wells and Fairouz Kamareddine. BNF-Style Notation as it is Actually Used
• [T24] Olaf Teschke, Vincent Stange, Moritz Schubotz, Norman Meuschke and Bela Gipp. Forms of Plagiarism in Digital Mathematical Libraries
• [T25] Moa Johansson. Lemma Discovery for Induction - A survey
• [T27] Claudio Sacerdoti Coen. A Coq plugin to export its libraries to XML
• [T29] Andrea Condoluci, Michael Kohlhase, Dennis Müller, Florian Rabe, Claudio Sacerdoti Coen and Makarius Wenzel. Relational Data Across Mathematical Libraries
• [T32] Florian Rabe and Yasmine Sharoda. Diagram Combinators in MMT
• [T34] Matthew England and Dorian Florescu. Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition
• [T39] William Farmer and Jacques Carette. Towards Specifying Symbolic Computation
• [T47] Daniel Raggi, Aaron Stockdill, Mateja Jamnik, Grecia Garcia Garcia, Holly Sutherland and Peter Cheng. Inspection and selection of representations
• [T49] Dennis Müller, Florian Rabe and Claudio Sacerdoti Coen. The Coq Library as a Theory Graph
• [T52] Besik Dundua, Temur Kutsia and Mircea Marin. Variadic Equational Matching

Workshop on Large Mathematical Libraries

• [LML1] Makarius Wenzel. Isabelle technology for the Archive of Formal Proofs with application to MMT
• [LML2] Claudio Sacerdoti Coen. Attempts at skinning an elephant
• [LML3] Wolfgang Dalitz, Wolfram Sperber, Moritz Schubotz, and Hagen Chrapary. alsoMATH - A Database for Mathematical Algorithms and Software
• [LML4] Gilles Dowek and François Thiré. Logipedia: a multi-system encyclopedia of formal proofs
• [LML5] Michael Kohlhase. The Data Aspect of Large Mathematical Libraries

Doctoral Programme

• [DP1] Sebastian Sahli. The MATh Tutor project
• [DP2] Frieder Simon. New Approaches to ATPs
• [DP3] Takuto Asakura. Understanding Scientific Documents with Synthetic Analysis on Mathematical Expressions and Natural Language
• [DP4] Joshua Chen. Hybrid and alternative logics in Isabelle
• [DP5] Jonas Betzendahl. Definedness Reasoning in Formal Mathematics and Theorem Proving
• [DP6] Max Rapp. A Unifying Framework for Managing Conflict-laden Content
• [DP7] Yasmine Sharoda. Leveraging Information Contained in a Theory Presentation
• [DP8] Tom Wiesing. Evolving MathHub for Tetrapodal Math
• [DP9] Qingxiang Wang. Automating Formalization of Mathematics with Machine Learning and Data Mining

Workshop on Formal Mathematics for Mathematicians (FMM)

• [FMM1] Chad Brown. Higher-Order Logic and Set Theory: Stronger Together
• [FMM2] Adam Naumowicz. Testing Mizar User Interactivity in a University-level Introductory Course on Foundations of Mathematics
• [FMM3] Michael Junk and Stefan Hölle. Numerical MMATh
• [FMM4] Peter Koepke. Textbook Mathematics in the Naproche-SAD System
• [FMM5] Artur Korniłowicz. Sethood Property in Mizar
• [FMM6] Adam Grabowski. Constructing Examples of Fuzzy Implications within the Mizar Mathematical Library
• [FMM7] Adrian Jaszczak. Formal Verification of the Correctness of Chosen Algorithms in Mizar
• [FMM8] Sofiene Tahar. Formalization of Dynamic Reliability Algebras in HOL

Work in Progress Presentations

• [WIP53] Luis Berlioz. Creating a Database of Definitions From Large Mathematical Corpora
• [WIP54] Alexandre Bouquet and Thierry Bouche. GDML : Grenoble Digital Mathematics Library
• [WIP59] Alexander Kirillovich, Olga Nevzorova, Marina Falileeva, Evgeny Lipachev and Liliana Shakirova. OntoMathEdu: Towards an Educational Mathematical Ontology

OpenMath Workshop

• [OM1] Lars Hellström. Formalising Riemann Surfaces
• [OM2] Tom Wiesing. Proposed Standard Extension: A JSON Binding for OpenMath
• [OM3] Florian Rabe. Variables: Local Scope vs. Alpha-Renaming
• [OM4] Michael Kohlhase. OpenMath Society Business Meeting
• [OM5] Moritz Schubotz. Wiki Math Community Group Meeting