Intelligent Computer Mathematics

1. Front Matter

   PDF

2. Invited Talks

   1. What International Studies Say about the Importance and Limitations of Using Computers to Teach Mathematics in Secondary Schools

      • Jaime Carvalho e Silva

      Pages 1-11

   2. Towards Robust Hyperlinks for Web-Based Scholarly Communication

      • Herbert Van de Sompel, Martin Klein, Harihar Shankar

      Pages 12-25

   3. Computable Data, Mathematics, and Digital Libraries in Mathematica and Wolfram|Alpha

      • Eric Weisstein

      Pages 26-29

3. Calculemus

   1. Towards the Formal Reliability Analysis of Oil and Gas Pipelines

      • Waqar Ahmad, Osman Hasan, Sofiène Tahar, Mohammad Salah Hamdi

      Pages 30-44

   2. Problem Formulation for Truth-Table Invariant Cylindrical Algebraic Decomposition by Incremental Triangular Decomposition

      • Matthew England, Russell Bradford, Changbo Chen, James H. Davenport, Marc Moreno Maza, David Wilson

      Pages 45-60

   3. A Tableaux-Based Decision Procedure for Multi-parameter Propositional Schemata

      • David Cerna

      Pages 61-75

   4. Detecting Unknots via Equational Reasoning, I: Exploration

      • Andrew Fish, Alexei Lisitsa

      Pages 76-91

   5. Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition

      • Zongyan Huang, Matthew England, David Wilson, James H. Davenport, Lawrence C. Paulson, James Bridge

      Pages 92-107

   6. Hipster: Integrating Theory Exploration in a Proof Assistant

      • Moa Johansson, Dan Rosén, Nicholas Smallbone, Koen Claessen

      Pages 108-122

   7. Formalization of Complex Vectors in Higher-Order Logic

      • Sanaz Khan Afshar, Vincent Aravantinos, Osman Hasan, Sofiène Tahar

      Pages 123-137

   8. A Mathematical Structure for Modeling Inventions

      • Bernd Wegner, Sigram Schindler

      Pages 138-152

4. Digital Mathematics Library

   1. Search Interfaces for Mathematicians

      • Andrea Kohlhase

      Pages 153-168

   2. A Data Model and Encoding for a Semantic, Multilingual Terminology of Mathematics

      • Michael Kohlhase

      Pages 169-183

   3. PDF/A-3u as an Archival Format for Accessible Mathematics

      • Ross Moore

      Pages 184-199

   4. Which One Is Better: Presentation-Based or Content-Based Math Search?

      • Minh-Quoc Nghiem, Giovanni Yoko Kristianto, Goran Topić, Akiko Aizawa

      Pages 200-212

   5. POS Tagging and Its Applications for Mathematics

      • Ulf Schöneberg, Wolfram Sperber

      Pages 213-223

   6. Mathoid: Robust, Scalable, Fast and Accessible Math Rendering for Wikipedia

      • Moritz Schubotz, Gabriel Wicke

      Pages 224-235

5. Mathematical Knowledge Management

   1. Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?

      • Marco B. Caminati, Manfred Kerber, Christoph Lange, Colin Rowat

      Pages 236-251

   2. Realms: A Structure for Consolidating Knowledge about Mathematical Theories

      • Jacques Carette, William M. Farmer, Michael Kohlhase

      Pages 252-266

This book constitutes the joint refereed proceedings of Calculemus 2014, Digital Mathematics Libraries, DML 2014, Mathematical Knowledge Management, MKM 2014 and Systems and Projects, S&P 2014, held in Coimbra, Portugal, during July 7-11, 2014 as four tracks of CICM 2014, the Conferences on Intelligent Computer Mathematics. The 26 full papers and 9 Systems and Projects descriptions presented together with 5 invited talks were carefully reviewed and selected from a total of 55 submissions. The Calculemus track of CICM examines the integration of symbolic computation and mechanized reasoning. The Digital Mathematics Libraries track - evolved from the DML workshop series - features math-aware technologies, standards, algorithms and processes towards the fulfillment of the dream of a global DML. The Mathematical Knowledge Management track of CICM is concerned with all aspects of managing mathematical knowledge in the informal, semi-formal and formal settings. The Systems and Projects track presents short descriptions of existing systems or on-going projects in the areas of all the other tracks of the conference.

• formal methods
• machine learning
• natural language processing
• search interface
• smilarity measures
• support vector machine
• theorem proving and SAT solving

• Computer Science Department, The University of Western Ontario, London, Canada

  Stephen M. Watt

• Departments of Computer Science and Mathematical Sciences, University of Bath, Bath, UK

  James H. Davenport

• School of Computer Science, Edgbaston, University of Birmingham, Birmingham, UK

  Alan P. Sexton

• Faculty of Informatics, Masaryk University, Brno, Czech Republic

  Petr Sojka

• Institute for Computing Sciences, Radboud University Nijmegen, Nijmegen, The Netherlands

  Josef Urban

Policies and ethics