Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings (Lecture Notes in Computer Science Book 10383)

This book constitutes the refereed proceedings of the 10th International Conference on Intelligent Computer Mathematics, CICM 2017, held in Edinburgh, Scotland, in July 2017. The 22 full papers and 3 abstracts of invited papers presented were carefully reviewed and selected from a total of 40 submissions. The papers are organized in three tracks: the Calculemus track examining the integration of symbolic computation and mechanized reasoning; the Digital Mathematics Libraries track dealing with math-aware technologies, standards, algorithms, and processes; the Mathematical Knowledge Management track being concerned with all aspects of managing mathematical knowledge, in informal, semi-formal, and formal settings. An additional track Systems and Projects contains descriptions of systems and relevant projects, both of which are key to a research topic where theory and practice interact on explicitly represented knowledge. Front Matter ....Pages I-XVIII DeepAlgebra - An Outline of a Program (Przemysław Chojecki)....Pages 1-8 Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study (Jacques Carette, William M. Farmer)....Pages 9-24 The Formalization of Vickrey Auctions: A Comparison of Two Approaches in Isabelle and Theorema (Alexander Maletzky, Wolfgang Windsteiger)....Pages 25-39 Automatically Proving Equivalence by Type-Safe Reflection (Franck Slama, Edwin Brady)....Pages 40-55 The Global Digital Mathematics Library and the International Mathematical Knowledge Trust (Patrick D. F. Ion, Stephen M. Watt)....Pages 56-69 The New Numdam Platform (Thierry Bouche, Olivier Labbe)....Pages 70-82 Classification of Alignments Between Concepts of Formal Mathematical Systems (Dennis Müller, Thibault Gauthier, Cezary Kaliszyk, Michael Kohlhase, Florian Rabe)....Pages 83-98 Software Citations, Information Systems, and Beyond (Michael Kohlhase, Wolfram Sperber)....Pages 99-114 Semantic Preserving Bijective Mappings of Mathematical Formulae Between Document Preparation Systems and Computer Algebra Systems (Howard S. Cohl, Moritz Schubotz, Abdou Youssef, André Greiner-Petter, Jürgen Gerhard, Bonita V. Saunders et al.)....Pages 115-131 Towards Mathematical AI via a Model of the Content and Process of Mathematical Question and Answer Dialogues (Joseph Corneli, Ursula Martin, Dave Murray-Rust, Alison Pease)....Pages 132-146 Theory Morphisms in Church’s Type Theory with Quotation and Evaluation (William M. Farmer)....Pages 147-162 Semantic Representation of General Topology in the Wolfram Language (Ian Ford)....Pages 163-177 Zeta Types and Tannakian Symbols as a Method for Representing Mathematical Knowledge (Andreas Holmstrom, Torstein Vik)....Pages 178-192 Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic (Cezary Kaliszyk, Karol Pąk)....Pages 193-207 Visual Structure in Mathematical Expressions (Andrea Kohlhase, Michael Kohlhase, Michael Fürsich)....Pages 208-223 Mathematical Models as Research Data via Flexiformal Theory Graphs (Michael Kohlhase, Thomas Koprucki, Dennis Müller, Karsten Tabelow)....Pages 224-238 A Verified Algorithm Enumerating Event Structures (Juliana Bowles, Marco B. Caminati)....Pages 239-254 Reasoning with Concept Diagrams About Antipatterns in Ontologies (Zohreh Shams, Mateja Jamnik, Gem Stapleton, Yuri Sato)....Pages 255-271 A Web-Based Toolkit for Mathematical Word Processing Applications with Semantics (Nathan C. Carter, Kenneth G. Monks)....Pages 272-291 ENIGMA: Efficient Learning-Based Inference Guiding Machine (Jan Jakubův, Josef Urban)....Pages 292-302 Proof Mining with Dependent Types (Ekaterina Komendantskaya, Jónathan Heras)....Pages 303-318 Formalization of Transform Methods Using HOL Light (Adnan Rashid, Osman Hasan)....Pages 319-332 Combining Refinement and Signal-Temporal Logic for Biological Systems (Usman Sanwal, Umair Siddique)....Pages 333-339 VMEXT: A Visualization Tool for Mathematical Expression Trees (Moritz Schubotz, Norman Meuschke, Thomas Hepp, Howard S. Cohl, Bela Gipp)....Pages 340-355 Part-of-Math Tagging and Applications (Abdou Youssef)....Pages 356-374 Back Matter ....Pages 375-375