TY  - BOOK
AU  - Carette,Jacques
AU  - Aspinall,David
AU  - Lange,Christoph
AU  - Sojka,Petr
AU  - Windsteiger,Wolfgang
TI  - Intelligent Computer Mathematics: MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings 
SN  - 9783642393204
PY  - 2013///
CY  - Berlin, Heidelberg
PB  - Springer Berlin Heidelberg
KW  - Computer science
KW  - Mathematical logic
KW  - Mathematics
KW  - Information Storage and Retrieval
KW  - Artificial intelligence
KW  - Text processing (Computer science)
N1  - 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
UR  - http://dx.doi.org/10.1007/978-3-642-39320-4
ER  -