| Contributions to AISC 2010 |
| The Challenges of Multivalued "Functions" (Keynote Talk) / James H. Davenport |
| The Dynamic Dictionary of Mathematical Functions (Keynote Talk) / Bruno Salvy |
| A Revisited Perspective on Symbolic Mathematical Computing and Artificial Intelligence (Keynote Talk) / Jacques Calmet ; John A. Campbell |
| I-Terms in Ordered Resolution and Superposition Calculi: Retrieving Lost Completeness / Hicham Bensaid ; Ricardo Caferra ; Nicolas Peltier |
| Structured Formal Development with Quotient Types in Isabelle/HOL / Maksym Bortin ; Christoph Lüth |
| Instantiation of SMT Problems Modulo Integers / Mnacho Echenim |
| On Krawtchouk Transforms / Philip Feinsilver ; René Schott |
| A Mathematical Model of the Competition between Acquired Immunity and Virus / Mikhail K. Kolev |
| Some Notes upon "When Does < T > Equal Sat (T)?" / Yongbin Li |
| How to Correctly Prune Tropical Trees / Jean-Vincent Loddo ; Luca Saiu |
| From Matrix Interpretations over the Rationals to Matrix Interpretations over the Naturals / Salvador Lucas |
| Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar / Josef Urban ; Geoff Sutcliffe |
| Contributions to Calculemus 2010 |
| Some Considerations on the Usability of Interactive Provers (Invited Talk) / Andrea Asperti ; Claudio Sacerdoti Coen |
| Mechanized Mathematics (Invited Talk) / Jacques Carette |
| Formal Proof of SCHUR Conjugate Function / Franck Butelle ; Florent Hivert ; Micaela Mayero ; Frédéric Toumazet |
| Symbolic Domain Decomposition / Alan P. Sexton ; Volker Sorge ; Stephen M. Watt |
| A Formal Quantifier Elimination for Algebraically Closed Fields / Cyril Cohen ; Assia Mahboubi |
| Computing in Coq with Infinite Algebraic Data Structures / César Domínguez ; Julio Rubio |
| Formally Verified Conditions for Regularity of Interval Matrices / Ioana Pasca |
| Reducing Expression Size Using Rule-Based Integration / David J. Jeffrey ; Albert D. Rich |
| A Unified Formal Description of Arithmetic and Set Theoretical Data Types / Paul Tarau |
| Contributions to MKM 2010 |
| Against Rigor (Invited Talk) / Doron Zeilberger |
| Smart Matching / Enrico Tassi |
| Electronic Geometry Textbook: A Geometric Textbook Knowledge Management System / Xiaoyu Chen |
| An OpenMath Content Dictionary for Tensor Concepts / Joseph B. Collins |
| On Duplication in Mathematical Repositories / Adam Grabowski ; Christoph Schwarzweller |
| Adapting Mathematical Domain Reasoners / Bastiaan Heeren ; Johan Jeuring |
| Integrating Multiple Sources to Answer Questions in Algebraic Topology / Jónathan Heras ; Vico Pascual ; Ana Romero |
| STEXIDE: An Integrated Development Environment for STEX Collections / Constantin Jucovschi ; Michael Kohlhase |
| Proofs, Proofs, Proofs, and Proofs / Manfred Kerber |
| Dimensions of Formality: A Case Study for MKM in Software Engineering / Andrea Kohlhase ; Christoph Lange |
| Towards MKM in the Large: Modular Representation and Scalable Software Architecture / Florian Rabe ; Vyacheslav Zholudev |
| The Formulator MathML Editor Project: User-Friendly Authoring of Content Markup Documents / Andriy Kovalchuk ; Vyachelav Levitsky ; Igor Samolyuk ; Valentyn Yanchuk |
| Notations Around the World: Census and Exploitation / Paul Libbrecht |
| Evidence Algorithm and System for Automated Deduction: A Retrospective View / Alexander Lyaletski ; Konstantin Verchinine |
| On Building a Knowledge Base for Stability Theory / Agnieszka Rowinska-Schwarzweller |
| Proviola: A Tool for Proof Re-animation / Carst Tankink ; Herman Geuvers ; James McKinna ; Freek Wiedijk |
| A Wiki for Mizar: Motivation, Considerations, and Initial Prototype / Jesse Alama ; Piotr Rudnicki |
| Author Index |
| Contributions to AISC 2010 |
| The Challenges of Multivalued "Functions" (Keynote Talk) / James H. Davenport |
| The Dynamic Dictionary of Mathematical Functions (Keynote Talk) / Bruno Salvy |
| A Revisited Perspective on Symbolic Mathematical Computing and Artificial Intelligence (Keynote Talk) / Jacques Calmet ; John A. Campbell |
| I-Terms in Ordered Resolution and Superposition Calculi: Retrieving Lost Completeness / Hicham Bensaid ; Ricardo Caferra ; Nicolas Peltier |
| Structured Formal Development with Quotient Types in Isabelle/HOL / Maksym Bortin ; Christoph Lüth |
