Intelligent Computer Mathematics : 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings

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