Intelligent Computer Mathematics  MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings /  [electronic resource] : 
edited by Jacques Carette, David Aspinall, Christoph Lange, Petr Sojka, Wolfgang Windsteiger. 
 - Berlin, Heidelberg :  Springer Berlin Heidelberg,  2013. 
 - 1 online resource (XVI, 384 p. 100 ill.) 
 - Lecture Notes in Computer Science,  7961  0302-9743 ; .
<br/><br/>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. 
<br/><br/><label>ISBN: </label>9783642393204 
<br/><br/><label>Subjects--Topical Terms: </label><br/>Computer science.<br/>Mathematical logic.<br/>Computer science--Mathematics.<br/>Information Storage and Retrieval.<br/>Artificial intelligence.<br/>Text processing (Computer science).