Abstract is missing.
- The Challenges of Multivalued Functions James H. Davenport. 1-12 [doi]
- The Dynamic Dictionary of Mathematical FunctionsBruno Salvy. 13 [doi]
- A Revisited Perspective on Symbolic Mathematical Computing and Artificial IntelligenceJacques Calmet, John A. Campbell. 14-18 [doi]
- ::::I::::-Terms in Ordered Resolution and Superposition Calculi: Retrieving Lost CompletenessHicham Bensaid, Ricardo Caferra, Nicolas Peltier. 19-33 [doi]
- Structured Formal Development with Quotient Types in Isabelle/HOLMaksym Bortin, Christoph Lüth. 34-48 [doi]
- Instantiation of SMT Problems Modulo IntegersMnacho Echenim, Nicolas Peltier. 49-63 [doi]
- On Krawtchouk TransformsPhilip Feinsilver, René Schott. 64-75 [doi]
- A Mathematical Model of the Competition between Acquired Immunity and VirusMikhail K. Kolev. 76-88 [doi]
- Some Notes upon When Does <T> Equal Sat(T)? Yongbin Li. 89-100 [doi]
- How to Correctly Prune Tropical TreesJean-Vincent Loddo, Luca Saiu. 101-115 [doi]
- From Matrix Interpretations over the Rationals to Matrix Interpretations over the NaturalsSalvador Lucas. 116-131 [doi]
- Automated Reasoning and Presentation Support for Formalizing Mathematics in MizarJosef Urban, Geoff Sutcliffe. 132-146 [doi]
- Some Considerations on the Usability of Interactive ProversAndrea Asperti, Claudio Sacerdoti Coen. 147-156 [doi]
- Mechanized MathematicsJacques Carette. 157 [doi]
- Formal Proof of SCHUR Conjugate FunctionFranck Butelle, Florent Hivert, Micaela Mayero, Frédéric Toumazet. 158-171 [doi]
- Symbolic Domain DecompositionJacques Carette, Alan P. Sexton, Volker Sorge, Stephen M. Watt. 172-188 [doi]
- A Formal Quantifier Elimination for Algebraically Closed FieldsCyril Cohen, Assia Mahboubi. 189-203 [doi]
- Computing in Coq with Infinite Algebraic Data StructuresCésar Domínguez, Julio Rubio. 204-218 [doi]
- Formally Verified Conditions for Regularity of Interval MatricesIoana Pasca. 219-233 [doi]
- Reducing Expression Size Using Rule-Based IntegrationDavid J. Jeffrey, Albert D. Rich. 234-246 [doi]
- A Unified Formal Description of Arithmetic and Set Theoretical Data TypesPaul Tarau. 247-261 [doi]
- Against RigorDoron Zeilberger. 262 [doi]
- Smart MatchingAndrea Asperti, Enrico Tassi. 263-277 [doi]
- Electronic Geometry Textbook: A Geometric Textbook Knowledge Management SystemXiaoyu Chen. 278-292 [doi]
- An OpenMath Content Dictionary for Tensor ConceptsJoseph B. Collins. 293-299 [doi]
- On Duplication in Mathematical RepositoriesAdam Grabowski, Christoph Schwarzweller. 300-314 [doi]
- Adapting Mathematical Domain ReasonersBastiaan Heeren, Johan Jeuring. 315-330 [doi]
- Integrating Multiple Sources to Answer Questions in Algebraic TopologyJónathan Heras, Vico Pascual, Ana Romero, Julio Rubio. 331-335 [doi]
- sTeXIIS: An Integrated Development Environment for sTeX CollectionsConstantin Jucovschi, Michael Kohlhase. 336-344 [doi]
- Proofs, Proofs, Proofs, and ProofsManfred Kerber. 345-354 [doi]
- Dimensions of Formality: A Case Study for MKM in Software EngineeringAndrea Kohlhase, Michael Kohlhase, Christoph Lange 0002. 355-369 [doi]
- Towards MKM in the Large: Modular Representation and Scalable Software ArchitectureMichael Kohlhase, Florian Rabe, Vyacheslav Zholudev. 370-384 [doi]
- Notations Around the World: Census and ExploitationPaul Libbrecht. 398-410 [doi]
- Evidence Algorithm and System for Automated Deduction: A Retrospective ViewAlexander V. Lyaletski, Konstantin Verchinine. 411-426 [doi]
- On Building a Knowledge Base for Stability TheoryAgnieszka Rowinska-Schwarzweller, Christoph Schwarzweller. 427-439 [doi]
- Proviola: A Tool for Proof Re-animationCarst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk. 440-454 [doi]
- A Wiki for Mizar: Motivation, Considerations, and Initial PrototypeJosef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers. 455-469 [doi]