Intelligent Computer Mathematics [electronic resource] : MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings / edited by Jacques Carette, David Aspinall, Christoph Lange, Petr Sojka, Wolfgang Windsteiger.

Calculemus -- The Rooster and the Butterflies -- Optimising Problem Formulation for Cylindrical Algebraic Decomposition -- The Formalization of Syntax-Based Mathematical Algorithms Using Quotation and Evaluation -- Certification of Bounds of Non-linear Functions: The Templates Method -- Verifying a Plaftorm for Digital Imaging: A Multi-tool Strategy -- A Universal Machine for Biform Theory Graphs -- MKM -- Mathematical Practice, Crowdsourcing, and Social Machines -- Automated Reasoning Service for HOL Light -- Understanding Branch Cuts of Expressions -- Formal Mathematics on Display: A Wiki for Flyspeck -- Determining Points on Handwritten Mathematical Symbols -- Capturing Hiproofs in HOL Light -- A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory -- Students' Comparison of Their Trigonometric Answers with the Answers of a Computer Algebra System -- DML -- Mathematics and the World Wide Web -- Structural Similarity Search for Mathematics Retrieval -- Towards Machine-Actionable Modules of a Digital Mathematics Library: The Example of DML-CZ -- A Hybrid Approach for Semantic Enrichment of MathML Mathematical Expressions -- Three Years of DLMF: Web, Math and Search -- Escaping the Trap of Too Precise Topic Queries -- Using MathML to Represent Units of Measurement for Improved Ontology Alignment -- Systems and Projects -- A Web Interface for Isabelle: The Next Generation -- The ForMaRE Project - Formal Mathematical Reasoning in Economics -- LATExml 2012 - A Year of LATExml -- The MMT API: A Generic MKM System -- Math-Net.Ru as a Digital Archive of the Russian Mathematical Knowledge from the XIX Century to Today -- A Dynamic Symbolic Geometry Environment Based on the GröbnerCover Algorithm for the Computation of Geometric Loci and Envelopes -- ML4PG in Computer Algebra Verification -- Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems -- The Web Geometry Laboratory Project -- swMATH - A New Information Service for Mathematical Software -- Software for Evaluating Relevance of Steps in Algebraic Transformations -- The DeLiVerMATH Project: Text Analysis in Mathematics.