Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings

Front Matter ....Pages i-xi
Front Matter ....Pages 1-1
 A Promising Path Towards Autoformalization and General Artificial Intelligence  (Christian Szegedy)....Pages 3-20
Front Matter ....Pages 21-21
 Formal Adventures in Convex and Conical Spaces  (Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa)....Pages 23-38
 Towards a Heterogeneous Query Language for Mathematical Knowledge  (Katja Berčič, Michael Kohlhase, Florian Rabe)....Pages 39-54
 Leveraging the Information Contained in Theory Presentations  (Jacques Carette, William M. Farmer, Yasmine Sharoda)....Pages 55-70
 Metamath Zero: Designing a Theorem Prover Prover  (Mario Carneiro)....Pages 71-88
 Adding an Abstraction Barrier to ZF Set Theory  (Ciarán Dunne, J. B. Wells, Fairouz Kamareddine)....Pages 89-104
 A Framework for Formal Dynamic Dependability Analysis Using HOL Theorem Proving  (Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar)....Pages 105-122
 Induction with Generalization in Superposition Reasoning  (Márton Hajdú, Petra Hozzová, Laura Kovács, Johannes Schoisswohl, Andrei Voronkov)....Pages 123-137
 A Survey of Languages for Formalizing Mathematics  (Cezary Kaliszyk, Florian Rabe)....Pages 138-156
 OntoMath\({}^{Edu}\): A Linguistically Grounded Educational Mathematical Ontology  (Alexander Kirillovich, Olga Nevzorova, Marina Falileeva, Evgeny Lipachev, Liliana Shakirova)....Pages 157-172
 FrameIT: Detangling Knowledge Management from Game Design in Serious Games  (Michael Kohlhase, Benjamin Bösl, Richard Marcus, Dennis Müller, Denis Rochau, Navid Roux et al.)....Pages 173-189
 Formalizing Graph Trail Properties in Isabelle/HOL  (Laura Kovács, Hanna Lachnitt, Stefan Szeider)....Pages 190-205
 Representing Structural Language Features in Formal Meta-languages  (Dennis Müller, Florian Rabe, Colin Rothgang, Michael Kohlhase)....Pages 206-221
 Formally Verifying Proofs for Algebraic Identities of Matrices  (Leonard Schmitz, Viktor Levandovskyy)....Pages 222-236
 AutoMSC: Automatic Assignment of Mathematics Subject Classification Labels  (Moritz Schubotz, Philipp Scharpf, Olaf Teschke, Andreas Kühnemund, Corinna Breitinger, Bela Gipp)....Pages 237-250
 Maintaining a Library of Formal Mathematics  (Floris van Doorn, Gabriel Ebner, Robert Y. Lewis)....Pages 251-267
Front Matter ....Pages 269-269
 The Tactician  (Lasse Blaauwbroek, Josef Urban, Herman Geuvers)....Pages 271-277
 Tree Neural Networks in HOL4  (Thibault Gauthier)....Pages 278-283
 Interpreting Mathematical Texts in Naproche-SAD  (Adrian De Lon, Peter Koepke, Anton Lorenzen)....Pages 284-289
 TGView3D: A System for 3-Dimensional Visualization of Theory Graphs  (Richard Marcus, Michael Kohlhase, Florian Rabe)....Pages 290-296
 Simple Dataset for Proof Method Recommendation in Isabelle/HOL  (Yutaka Nagashima)....Pages 297-302
 Dataset Description: Formalization of Elementary Number Theory in Mizar  (Adam Naumowicz)....Pages 303-308
 Guiding Inferences in Connection Tableau by Recurrent Neural Networks  (Bartosz Piotrowski, Josef Urban)....Pages 309-314
 First Neural Conjecturing Datasets and Experiments  (Josef Urban, Jan Jakubův)....Pages 315-323
 A Contextual and Labeled Math-Dataset Derived from NIST’s DLMF  (Abdou Youssef, Bruce R. Miller)....Pages 324-330
Back Matter ....Pages 331-337