MKM/Calculemus/DML

Publications

2013

Cezary Kaliszyk, Josef Urban
Automated Reasoning Service for HOL Light. MKM/Calculemus/DML (2013)
Patrick D. F. Ion
Mathematics and the World Wide Web. MKM/Calculemus/DML (2013)
Jónathan Heras, Ekaterina Komendantskaya
ML4PG in Computer Algebra Verification. MKM/Calculemus/DML (2013)
Matthew England, Russell J. Bradford, James H. Davenport, David J. Wilson
Understanding Branch Cuts of Expressions. MKM/Calculemus/DML (2013)
Jónathan Heras, Gadea Mata, Ana Romero, Julio Rubio, Rubén Sáenz
Verifying a Plaftorm for Digital Imaging: A Multi-tool Strategy. MKM/Calculemus/DML (2013)
Rein Prank
Software for Evaluating Relevance of Steps in Algebraic Transformations. MKM/Calculemus/DML (2013)
Xavier Allamigeon, Stéphane Gaubert, Victor Magron, Benjamin Werner
Certification of Bounds of Non-linear Functions: The Templates Method. MKM/Calculemus/DML (2013)
William M. Farmer
The Formalization of Syntax-Based Mathematical Algorithms Using Quotation and Evaluation. MKM/Calculemus/DML (2013)
Deyan Ginev, Bruce R. Miller
2012 - A Year of. MKM/Calculemus/DML (2013)
Christoph Lange, Marco B. Caminati, Manfred Kerber, Till Mossakowski, Colin Rowat, Makarius Wenzel, Wolfgang Windsteiger
A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory. MKM/Calculemus/DML (2013)
Bruno Barras, Lourdes Del Carmen González-Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems. MKM/Calculemus/DML (2013)
Chau Do, Eric J. Pauwels
Using MathML to Represent Units of Measurement for Improved Ontology Alignment. MKM/Calculemus/DML (2013)
Michal Ruzicka, Petr Sojka, Vlastimil Krejcír
Towards Machine-Actionable Modules of a Digital Mathematics Library - The Example of DML-CZ. MKM/Calculemus/DML (2013)
Ursula Martin, Alison Pease
Mathematical Practice, Crowdsourcing, and Social Machines. MKM/Calculemus/DML (2013)
Ulf Schöneberg, Wolfram Sperber
The DeLiVerMATH Project - Text Analysis in Mathematics. MKM/Calculemus/DML (2013)
Minh-Quoc Nghiem, Giovanni Yoko Kristianto, Goran Topic, Akiko Aizawa
A Hybrid Approach for Semantic Enrichment of MathML Mathematical Expressions. MKM/Calculemus/DML (2013)
Dmitry E. Chebukov, Alexander D. Izaak, Olga G. Misyurina, Yuri A. Pupyrev, Alexey B. Zhizhchenko
Math-Net.Ru as a Digital Archive of the Russian Mathematical Knowledge from the XIX Century to Today. MKM/Calculemus/DML (2013)
Sebastian Bönisch, Michael Brickenstein, Hagen Chrapary, Gert-Martin Greuel, Wolfram Sperber
swMATH - A New Information Service for Mathematical Software. MKM/Calculemus/DML (2013)
Eno Tõnisson
Students' Comparison of Their Trigonometric Answers with the Answers of a Computer Algebra System. MKM/Calculemus/DML (2013)
Pedro Quaresma, Vanda Santos, Seifeddine Bouallegue
The Web Geometry Laboratory Project. MKM/Calculemus/DML (2013)
Christoph Lange, Colin Rowat, Manfred Kerber
The ForMaRE Project - Formal Mathematical Reasoning in Economics. MKM/Calculemus/DML (2013)
Michael Kohlhase, Felix Mance, Florian Rabe
A Universal Machine for Biform Theory Graphs. MKM/Calculemus/DML (2013)
Assia Mahboubi
The Rooster and the Butterflies. MKM/Calculemus/DML (2013)
Bruce R. Miller
Three Years of DLMF: Web, Math and Search. MKM/Calculemus/DML (2013)
Russell J. Bradford, James H. Davenport, Matthew England, David J. Wilson
Optimising Problem Formulation for Cylindrical Algebraic Decomposition. MKM/Calculemus/DML (2013)
Paul Libbrecht
Escaping the Trap of Too Precise Topic Queries. MKM/Calculemus/DML (2013)
Shahab Kamali, Frank Wm. Tompa
Structural Similarity Search for Mathematics Retrieval. MKM/Calculemus/DML (2013)
Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers
Formal Mathematics on Display: A Wiki for Flyspeck. MKM/Calculemus/DML (2013)
Christoph Lüth, Martin Ring
A Web Interface for Isabelle: The Next Generation. MKM/Calculemus/DML (2013)
Steven Obua, Mark Adams, David Aspinall
Capturing Hiproofs in HOL Light. MKM/Calculemus/DML (2013)
Miguel A. Abánades, Francisco Botana
A Dynamic Symbolic Geometry Environment Based on the GröbnerCover Algorithm for the Computation of Geometric Loci and Envelopes. MKM/Calculemus/DML (2013)
Rui Hu, Stephen M. Watt
Determining Points on Handwritten Mathematical Symbols. MKM/Calculemus/DML (2013)
Florian Rabe
The MMT API: A Generic MKM System. MKM/Calculemus/DML (2013)

volume 7961, 2013

Intelligent Computer Mathematics - MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings MKM/Calculemus/DML 7961 (2013)