Abstract is missing.
- The Rooster and the ButterfliesAssia Mahboubi. 1-18 [doi]
- Optimising Problem Formulation for Cylindrical Algebraic DecompositionRussell J. Bradford, James H. Davenport, Matthew England, David J. Wilson. 19-34 [doi]
- The Formalization of Syntax-Based Mathematical Algorithms Using Quotation and EvaluationWilliam M. Farmer. 35-50 [doi]
- Certification of Bounds of Non-linear Functions: The Templates MethodXavier Allamigeon, Stéphane Gaubert, Victor Magron, Benjamin Werner. 51-65 [doi]
- Verifying a Plaftorm for Digital Imaging: A Multi-tool StrategyJónathan Heras, Gadea Mata, Ana Romero, Julio Rubio, Rubén Sáenz. 66-81 [doi]
- A Universal Machine for Biform Theory GraphsMichael Kohlhase, Felix Mance, Florian Rabe. 82-97 [doi]
- Mathematical Practice, Crowdsourcing, and Social MachinesUrsula Martin, Alison Pease. 98-119 [doi]
- Automated Reasoning Service for HOL LightCezary Kaliszyk, Josef Urban. 120-135 [doi]
- Understanding Branch Cuts of ExpressionsMatthew England, Russell J. Bradford, James H. Davenport, David J. Wilson. 136-151 [doi]
- Formal Mathematics on Display: A Wiki for FlyspeckCarst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers. 152-167 [doi]
- Determining Points on Handwritten Mathematical SymbolsRui Hu, Stephen M. Watt. 168-183 [doi]
- Capturing Hiproofs in HOL LightSteven Obua, Mark Adams, David Aspinall. 184-199 [doi]
- A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction TheoryChristoph Lange 0002, Marco B. Caminati, Manfred Kerber, Till Mossakowski, Colin Rowat, Makarius Wenzel, Wolfgang Windsteiger. 200-215 [doi]
- Students' Comparison of Their Trigonometric Answers with the Answers of a Computer Algebra SystemEno Tõnisson. 216-229 [doi]
- Mathematics and the World Wide WebPatrick D. F. Ion. 230-245 [doi]
- Structural Similarity Search for Mathematics RetrievalShahab Kamali, Frank Wm. Tompa. 246-262 [doi]
- Towards Machine-Actionable Modules of a Digital Mathematics Library - The Example of DML-CZMichal Ruzicka, Petr Sojka, Vlastimil Krejcír. 263-277 [doi]
- A Hybrid Approach for Semantic Enrichment of MathML Mathematical ExpressionsMinh-Quoc Nghiem, Giovanni Yoko Kristianto, Goran Topic, Akiko Aizawa. 278-287 [doi]
- Three Years of DLMF: Web, Math and SearchBruce R. Miller. 288-295 [doi]
- Escaping the Trap of Too Precise Topic QueriesPaul Libbrecht. 296-309 [doi]
- Using MathML to Represent Units of Measurement for Improved Ontology AlignmentChau Do, Eric J. Pauwels. 310-325 [doi]
- A Web Interface for Isabelle: The Next GenerationChristoph Lüth, Martin Ring. 326-329 [doi]
- The ForMaRE Project - Formal Mathematical Reasoning in EconomicsChristoph Lange 0002, Colin Rowat, Manfred Kerber. 330-334 [doi]
- 2012 - A Year ofDeyan Ginev, Bruce R. Miller. 335-338 [doi]
- The MMT API: A Generic MKM SystemFlorian Rabe. 339-343 [doi]
- Math-Net.Ru as a Digital Archive of the Russian Mathematical Knowledge from the XIX Century to TodayDmitry E. Chebukov, Alexander D. Izaak, Olga G. Misyurina, Yuri A. Pupyrev, Alexey B. Zhizhchenko. 344-348 [doi]
- A Dynamic Symbolic Geometry Environment Based on the GröbnerCover Algorithm for the Computation of Geometric Loci and EnvelopesMiguel A. Abánades, Francisco Botana. 349-353 [doi]
- ML4PG in Computer Algebra VerificationJónathan Heras, Ekaterina Komendantskaya. 354-358 [doi]
- Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving SystemsBruno Barras, Lourdes Del Carmen González-Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff. 359-363 [doi]
- The Web Geometry Laboratory ProjectPedro Quaresma, Vanda Santos, Seifeddine Bouallegue. 364-368 [doi]
- swMATH - A New Information Service for Mathematical SoftwareSebastian Bönisch, Michael Brickenstein, Hagen Chrapary, Gert-Martin Greuel, Wolfram Sperber. 369-373 [doi]
- Software for Evaluating Relevance of Steps in Algebraic TransformationsRein Prank. 374-378 [doi]
- The DeLiVerMATH Project - Text Analysis in MathematicsUlf Schöneberg, Wolfram Sperber. 379-382 [doi]