Abstract is missing.
- Computational Logic and Continuous Mathematics, Pure and AppliedRob Arthan. 1 [doi]
- Math-Literate ComputersDorothea Blostein. 2-13 [doi]
- Abstraction-Based Information Technology: A Framework for Open Mechanized ReasoningJacques Calmet. 14-26 [doi]
- Software Engineering for MathematicsGeorges Gonthier. 27 [doi]
- Some Traditional Mathematical Knowledge ManagementPatrick D. F. Ion. 28 [doi]
- Math Handwriting Recognition in Windows 7 and Its BenefitsMarko Panic. 29-30 [doi]
- Assembling the Digital Mathematics LibraryDavid Ruddy. 31 [doi]
- CAMAL 40 Years on - Is Small Still Beautiful?John Fitch. 32-44 [doi]
- Conservative Retractions of Propositional Logic Theories by Means of Boolean Derivatives: Theoretical FoundationsGonzalo A. Aranda-Corral, JoaquÃn Borrego-DÃaz, M. Magdalena Fernández-Lebrón. 45-58 [doi]
- Combining Coq and Gappa for Certifying Floating-Point ProgramsSylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond. 59-74 [doi]
- A Comparison of Equality in Computer Algebra and Correctness in Mathematical PedagogyRussell J. Bradford, James H. Davenport, Christopher J. Sangwin. 75-89 [doi]
- Exploring a Quantum Theory with Graph Rewriting and Computer AlgebraAleks Kissinger. 90-105 [doi]
- ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo SystemFrancisco-Jesús MartÃn-Mateos, Julio Rubio, José-Luis Ruiz-Reina. 106-121 [doi]
- Combined Decision Techniques for the Existential Theory of the RealsGrant Olney Passmore, Paul B. Jackson. 122-137 [doi]
- Reasoning with Generic Cases in the Arithmetic of Abstract MatricesAlan P. Sexton, Volker Sorge, Stephen M. Watt. 138-153 [doi]
- Invariant Properties of Third-Order Non-hyperbolic Linear Partial Differential OperatorsEkaterina Shemyakova. 154-169 [doi]
- A Groupoid of Isomorphic Data TransformationsPaul Tarau. 170-185 [doi]
- Algorithms for the Functional Decomposition of Laurent PolynomialsStephen M. Watt. 186-200 [doi]
- A Linear Grammar Approach to Mathematical Formula Recognition from PDFJosef B. Baker, Alan P. Sexton, Volker Sorge. 201-216 [doi]
- Formal Proof: Reconciling Correctness and UnderstandingCristian S. Calude, Christine Müller. 217-232 [doi]
- A Review of Mathematical Knowledge ManagementJacques Carette, William M. Farmer. 233-246 [doi]
- OpenMath Content Dictionaries for SI Quantities and UnitsJoseph B. Collins. 247-262 [doi]
- Unifying Math Ontologies: A Tale of Two StandardsJames H. Davenport, Michael Kohlhase. 263-278 [doi]
- Integrating Web Services into Active Mathematical DocumentsJana Giceva, Christoph Lange 0002, Florian Rabe. 279-293 [doi]
- Representation for Interactive ExercisesGeorge Goguadze. 294-309 [doi]
- The Characteristics of Writing Environments for Mathematics: Behavioral Consequences and Implications for Software Design and UsabilityDavood G. Gozli, Marco Pollanen, Michael Reynolds. 310-324 [doi]
- Canonical Forms in Interactive Exercise AssistantsBastiaan Heeren, Johan Jeuring. 325-340 [doi]
- Spreadsheet Interaction with Frames: Exploring a Mathematical PracticeAndrea Kohlhase, Michael Kohlhase. 341-356 [doi]
- Compensating the Computational Bias of Spreadsheets with MKM TechniquesAndrea Kohlhase, Michael Kohlhase. 357-372 [doi]
- MathLang Translation to Isabelle SyntaxRobert Lamar, Fairouz Kamareddine, J. B. Wells. 373-388 [doi]
- A Mathematical Approach to Ontology Authoring and DocumentationChristoph Lange 0002, Michael Kohlhase. 389-404 [doi]
- A Logically Saturated Extension of Lionel Elie Mamane, Herman Geuvers, James McKinna. 405-421 [doi]
- From Tessellations to Table InterpretationRamana C. Jandhyala, Mukkai S. Krishnamoorthy, George Nagy, Raghav K. Padmanabhan, Sharad C. Seth, William Silversmith. 422-437 [doi]
- Finite Groups Representation Theory with CoqSidi Ould Biha. 438-452 [doi]
- Collaborative Assistant to Handle MathML ExpressionsAslam Muhammad, Ana MarÃa MartÃnez EnrÃquez, Gonzalo Escalada-Imaz. 453-459 [doi]
- Confidence Measures in Recognizing Handwritten Mathematical SymbolsOleg Golubitsky, Stephen M. Watt. 460-466 [doi]
- Using Open Mathematical Documents to Interface Computer Algebra and Proof Assistant SystemsJónathan Heras, Vico Pascual, Julio Rubio. 467-473 [doi]
- OpenMath in SCIEnce: SCSCP and POPCORNPeter Horn, Dan Roozemond. 474-479 [doi]
- A Knowledge Repository for Indefinite Integration Based on Transformation RulesA. D. Rich, David J. Jeffrey. 480-485 [doi]
- Natural Deduction Environment for MatitaClaudio Sacerdoti Coen, Enrico Tassi. 486-491 [doi]