Abstract is missing.
- Executing in Common Lisp, Proving in ACL2Mirian Andrés, Laureano Lambán, Julio Rubio. 1-12 [doi]
- A Rational Reconstruction of a System for Experimental MathematicsJacques Carette, William M. Farmer, Volker Sorge. 13-26 [doi]
- Context Aware Calculation and DeductionAmine Chaieb, Makarius Wenzel. 27-39 [doi]
- Towards Constructive Homological Algebra in Type TheoryThierry Coquand, Arnaud Spiwack. 40-54 [doi]
- What Might Understand a Function Mean?James H. Davenport. 55-65 [doi]
- Biform Theories in ChironWilliam M. Farmer. 66-79 [doi]
- Automatic Synthesis of Decision Procedures: A Case Study of Ground and Linear ArithmeticPredrag Janicic, Alan Bundy. 80-93 [doi]
- Certified Computer Algebra on Top of an Interactive Theorem ProverCezary Kaliszyk, Freek Wiedijk. 94-105 [doi]
- Quantifier Elimination for Approximate Factorization of Linear Partial Differential OperatorsElena Kartashova, Scott McCallum. 106-115 [doi]
- Rule-Based Simplification in Vector-Product SpacesSongxin Liang, David J. Jeffrey. 116-127 [doi]
- Mathematics and Scientific MarkupPeter Murray-Rust. 128-129 [doi]
- The On-Line Encyclopedia of Integer SequencesNeil J. A. Sloane. 130 [doi]
- First Steps on Using OpenMath to Add Proving Capabilities to Standard Dynamic Geometry SystemsMiguel A. Abánades, Jesús Escribano, Francisco Botana. 131-145 [doi]
- Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality CaseAndrea Asperti, Enrico Tassi. 146-160 [doi]
- A Framework for Interactive ProofDavid Aspinall, Christoph Lüth, Daniel Winterstein. 161-175 [doi]
- Supporting User-Defined Notations When Integrating Scientific Text-Editors with Proof Assistance SystemsSerge Autexier, Armin Fiedler, Thomas Neumann 0006, Marc Wagner. 176-190 [doi]
- Mizar Course in Logic and Set TheoryEwa Borak, Anna Zalewska. 191-204 [doi]
- Using Formal Concept Analysis in Mathematical DiscoverySimon Colton, Daniel Wagner. 205-220 [doi]
- Cooperative Repositories for Formal ProofsPierre Corbineau, Cezary Kaliszyk. 221-234 [doi]
- Revisions as an Essential Tool to Maintain Mathematical RepositoriesAdam Grabowski, Christoph Schwarzweller. 235-249 [doi]
- The Layers of LogiwebKlaus Grue. 250-264 [doi]
- Formal Representation of Mathematics in a Dependently Typed Set TheoryFeryal Fulya Horozal, Chad E. Brown. 265-279 [doi]
- Restoring Natural Language as a Computerised Mathematics Input MethodFairouz Kamareddine, Robert Lamar, Manuel Maarek, J. B. Wells. 280-295 [doi]
- Narrative Structure of Mathematical TextsFairouz Kamareddine, Manuel Maarek, Krzysztof Retel, J. B. Wells. 296-312 [doi]
- ::::Re:::: examining the MKM Value Proposition: From Math Web Search to Math Web ::::Re:::: SearchAndrea Kohlhase, Michael Kohlhase. 313-326 [doi]
- Alternative Aggregates in MizarGilbert Lee, Piotr Rudnicki. 327-341 [doi]
- An Approach to Mathematical Search Through Query Formulation and Data NormalizationRobert Miner, Rajesh Munavalli. 342-355 [doi]
- Extended Formula Normalization for ::::epsilon:::: -Retrieval and Sharing of Mathematical KnowledgeImmanuel Normann, Michael Kohlhase. 356-370 [doi]
- Towards Mathematical Knowledge Management for Electrical EngineeringAgnieszka Rowinska-Schwarzweller, Christoph Schwarzweller. 371-380 [doi]
- Spurious Disambiguation Error DetectionClaudio Sacerdoti Coen, Stefano Zacchiroli. 381-392 [doi]
- Methods of Relevance Ranking and Hit-content Generation in Math SearchAbdou Youssef. 393-406 [doi]