You must enable JavaScript to use this site
-
List of EventsInvited 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
|
-
News
- tentative informal proceedings
- formal proceedings online
- detailed program online
- 3 invited speakers
- accepted papers announced
- registration open
- extended deadline
- four workshops and tutorial confirmed
- LNAI proceedings confirmed
- initial program committee
- initial website online
Privacy policy and legal information
Last modified: August 22 2024 13:35:31 CEST