Skip to main content
SpringerLink
Log in
Book cover

Intelligent Computer Mathematics

MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013, Proceedings

  • Conference proceedings
  • © 2013

Overview

Editors:
  1. Jacques Carette

    1. Computing and Software, McMaster University, Hamilton, Canada

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. David Aspinall

    1. School of Informatics, University of Edinburgh, Edinburgh, Scotland, UK

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. Christoph Lange

    1. School of Computer Science, University of Birmingham, Birmingham, UK

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  4. Petr Sojka

    1. Faculty of Informatics, Department of Computer Graphics and Design, Masaryk University, Brno, Czech Republic

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  5. Wolfgang Windsteiger

    1. Johannes Kepler University Linz (JKU), RISC, Linz, Austria

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  • State of the art research of conference CICM 2013

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 7961)

Part of the book sub series: Lecture Notes in Artificial Intelligence (LNAI)

Included in the following conference series:

Conference proceedings info: CICM 2013.

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (33 papers)

  1. Front Matter

    Download chapter PDF

  2. Calculemus

    1. The Rooster and the Butterflies

      • Assia Mahboubi
      Pages 1-18

    2. Optimising Problem Formulation for Cylindrical Algebraic Decomposition

      • Russell Bradford, James H. Davenport, Matthew England, David Wilson
      Pages 19-34

    3. The Formalization of Syntax-Based Mathematical Algorithms Using Quotation and Evaluation

      • William M. Farmer
      Pages 35-50

    4. Certification of Bounds of Non-linear Functions: The Templates Method

      • Xavier Allamigeon, Stéphane Gaubert, Victor Magron, Benjamin Werner
      Pages 51-65

    5. Verifying a Plaftorm for Digital Imaging: A Multi-tool Strategy

      • Jónathan Heras, Gadea Mata, Ana Romero, Julio Rubio, Rubén Sáenz
      Pages 66-81

    6. A Universal Machine for Biform Theory Graphs

      • Michael Kohlhase, Felix Mance, Florian Rabe
      Pages 82-97

  3. MKM

    1. Mathematical Practice, Crowdsourcing, and Social Machines

      • Ursula Martin, Alison Pease
      Pages 98-119

    2. Automated Reasoning Service for HOL Light

      • Cezary Kaliszyk, Josef Urban
      Pages 120-135

    3. Understanding Branch Cuts of Expressions

      • Matthew England, Russell Bradford, James H. Davenport, David Wilson
      Pages 136-151

    4. Formal Mathematics on Display: A Wiki for Flyspeck

      • Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers
      Pages 152-167

    5. Determining Points on Handwritten Mathematical Symbols

      • Rui Hu, Stephen M. Watt
      Pages 168-183

    6. Capturing Hiproofs in HOL Light

      • Steven Obua, Mark Adams, David Aspinall
      Pages 184-199

    7. A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory

      • Christoph Lange, Marco B. Caminati, Manfred Kerber, Till Mossakowski, Colin Rowat, Makarius Wenzel et al.
      Pages 200-215

    8. Students’ Comparison of Their Trigonometric Answers with the Answers of a Computer Algebra System

      • Eno Tonisson
      Pages 216-229

  4. DML

    1. Mathematics and the World Wide Web

      • Patrick D. F. Ion
      Pages 230-245

    2. Structural Similarity Search for Mathematics Retrieval

      • Shahab Kamali, Frank Wm. Tompa
      Pages 246-262

    3. Towards Machine-Actionable Modules of a Digital Mathematics Library

      • Michal Růžička, Petr Sojka, Vlastimil Krejčíř
      Pages 263-277

    4. A Hybrid Approach for Semantic Enrichment of MathML Mathematical Expressions

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

    5. Three Years of DLMF: Web, Math and Search

      • Bruce R. Miller
      Pages 288-295
Back to top

Other volumes

  1. Intelligent Computer Mathematics

Keywords

About this book

This book constitutes the joint refereed proceedings of the 20th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2013, 6th International Workshop on Digital Mathematics Libraries, DML 2013, Systems and Projects, held in Bath, UK as part of CICM 2013, the Conferences on Intelligent Computer Mathematics. The 7 revised full papers out of 18 submissions for MKM 2013, 5 revised full papers out of 12 submissions for Calculemus 2013, 6 revised full papers out of 8 submissions for DML 2013, and 12 revised full papers out of 16 submissions for Systems and Project track presented together with 3 invited talks were carefully reviewed and selected, resulting in 33 papers from a total of 73 submissions.

Editors and Affiliations

  • Computing and Software, McMaster University, Hamilton, Canada

    Jacques Carette

  • School of Informatics, University of Edinburgh, Edinburgh, Scotland, UK

    David Aspinall

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

    Christoph Lange

  • Faculty of Informatics, Department of Computer Graphics and Design, Masaryk University, Brno, Czech Republic

    Petr Sojka

  • Johannes Kepler University Linz (JKU), RISC, Linz, Austria

    Wolfgang Windsteiger

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation