فهرست مطالب :
Front Matter ....Pages I-XII
System Description: XSL-Based Translator of Mizar to LaTeX (Grzegorz Bancerek, Adam Naumowicz, Josef Urban)....Pages 1-6
Translating the IMPS Theory Library to MMT/OMDoc (Jonas Betzendahl, Michael Kohlhase)....Pages 7-22
Using the Isabelle Ontology Framework (Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, Burkhart Wolff)....Pages 23-38
Automated Symbolic and Numerical Testing of DLMF Formulae Using Computer Algebra Systems (Howard S. Cohl, André Greiner-Petter, Moritz Schubotz)....Pages 39-52
Concrete Semantics with Coq and CoqHammer (Łukasz Czajka, Burak Ekici, Cezary Kaliszyk)....Pages 53-59
Automated Determination of Isoptics with Dynamic Geometry (Thierry Dana-Picard, Zoltán Kovács)....Pages 60-75
Biform Theories: Project Description (Jacques Carette, William M. Farmer, Yasmine Sharoda)....Pages 76-86
A Coq Formalization of Digital Filters (Diane Gallois-Wong, Sylvie Boldo, Thibault Hilaire)....Pages 87-103
MathTools: An Open API for Convenient MathML Handling (André Greiner-Petter, Moritz Schubotz, Howard S. Cohl, Bela Gipp)....Pages 104-110
Aligator.jl – A Julia Package for Loop Invariant Generation (Andreas Humenberger, Maximilian Jaroschek, Laura Kovács)....Pages 111-117
Enhancing ENIGMA Given Clause Guidance (Jan Jakubův, Josef Urban)....Pages 118-124
Formalized Mathematical Content in Lecture Notes on Modelling and Analysis (Michael Junk, Stefan Hölle, Sebastian Sahli)....Pages 125-130
Isabelle Import Infrastructure for the Mizar Mathematical Library (Cezary Kaliszyk, Karol Pąk)....Pages 131-146
Discourse Phenomena in Mathematical Documents (Andrea Kohlhase, Michael Kohlhase, Taweechai Ouypornkochagorn)....Pages 147-163
Finding and Proving New Geometry Theorems in Regular Polygons with Dynamic Geometry and Automated Reasoning Tools (Zoltán Kovács)....Pages 164-177
Gröbner Bases of Modules and Faugère’s \\(F_4\\) Algorithm in Isabelle/HOL (Alexander Maletzky, Fabian Immler)....Pages 178-193
MathChat: Computational Mathematics via a Social Machine (Manfred Minimair)....Pages 194-208
Automatically Finding Theory Morphisms for Knowledge Management (Dennis Müller, Michael Kohlhase, Florian Rabe)....Pages 209-224
Goal-Oriented Conjecturing for Isabelle/HOL (Yutaka Nagashima, Julian Parsert)....Pages 225-231
Knowledge Amalgamation for Computational Science and Engineering (Theresa Pollinger, Michael Kohlhase, Harald Köstler)....Pages 232-247
Validating Mathematical Theorems and Algorithms with RISCAL (Wolfgang Schreiner)....Pages 248-254
First Experiments with Neural Translation of Informal to Formal Mathematics (Qingxiang Wang, Cezary Kaliszyk, Josef Urban)....Pages 255-270
Deep Learning for Math Knowledge Processing (Abdou Youssef, Bruce R. Miller)....Pages 271-286
Back Matter ....Pages 287-287