Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings (Lecture Notes in Artificial Intelligence Book 12236)

This book constitutes the refereed proceedings of the 13th International Conference on Intelligent Computer Mathematics, CICM 2020, held in Bertinoro, Italy, in July 2020*. The 15 full papers, 1 invited paper and 2 abstracts of invited papers presented were carefully reviewed and selected from a total of 35 submissions. The papers focus on advances in automated theorem provers and formalization, computer algebra systems and their libraries, and applications of machine learning, among other topics. * The conference was held virtually due to the COVID-19 pandemic. -- Provided by publisher 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