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