Intelligent Computer Mathematics

1. Front Matter

   PDF

2. Joint Invited Talks

   1. Computational Logic and Continuous Mathematics, Pure and Applied

      • Rob Arthan

      Pages 1-1

   2. Math-Literate Computers

      • Dorothea Blostein

      Pages 2-13

   3. Abstraction-Based Information Technology: A Framework for Open Mechanized Reasoning

      • Jacques Calmet

      Pages 14-26

   4. Software Engineering for Mathematics

      • Georges Gonthier

      Pages 27-27

3. Calculemus Talks

   1. Some Traditional Mathematical Knowledge Management

      • Patrick D. F. Ion

      Pages 28-28

   2. Math Handwriting Recognition in Windows 7 and Its Benefits

      • Marko Panic

      Pages 29-30

   3. Assembling the Digital Mathematics Library

      • David Ruddy

      Pages 31-31

   4. CAMAL 40 Years on – Is Small Still Beautiful?

      • John Fitch

      Pages 32-44

   5. Conservative Retractions of Propositional Logic Theories by Means of Boolean Derivatives: Theoretical Foundations

      • Gonzalo A. Aranda-Corral, Joaquín Borrego-Díaz, M. Magdalena Fernández-Lebrón

      Pages 45-58

   6. Combining Coq and Gappa for Certifying Floating-Point Programs

      • Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond

      Pages 59-74

   7. A Comparison of Equality in Computer Algebra and Correctness in Mathematical Pedagogy

      • Russell Bradford, James H. Davenport, Christopher J. Sangwin

      Pages 75-89

   8. Exploring a Quantum Theory with Graph Rewriting and Computer Algebra

      • Aleks Kissinger

      Pages 90-105

   9. ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System

      • Francisco-Jesus Martín-Mateos, Julio Rubio, Jose-Luis Ruiz-Reina

      Pages 106-121

   10. Combined Decision Techniques for the Existential Theory of the Reals

       • Grant Olney Passmore, Paul B. Jackson

       Pages 122-137

   11. Reasoning with Generic Cases in the Arithmetic of Abstract Matrices

       • Alan P. Sexton, Volker Sorge, Stephen M. Watt

       Pages 138-153

   12. Invariant Properties of Third-Order Non-hyperbolic Linear Partial Differential Operators

       • Ekaterina Shemyakova

       Pages 154-169

   13. A Groupoid of Isomorphic Data Transformations

       • Paul Tarau

       Pages 170-185

   14. Algorithms for the Functional Decomposition of Laurent Polynomials

       • Stephen M. Watt

       Pages 186-200

4. MKM Talks

   1. A Linear Grammar Approach to Mathematical Formula Recognition from PDF

      • Josef B. Baker, Alan P. Sexton, Volker Sorge

      Pages 201-216

As computers and communications technology advance, greater opportunities arise for intelligent mathematical computation. While computer algebra, au- mated deduction and mathematical publishing each have long and successful histories, we are now seeing increasing opportunities for synergy among them. The Conferences on Intelligent Computer Mathematics (cicm 2009) is a c- lection of co-located meetings, allowing researchers and practitioners active in these related areas to share recent results and identify the next challenges. The speci?c areas of the cicm conferences and workshops are described below, but the unifying theme is the computerized handling of mathematical knowledge. The successful formalization of much of mathematics, as well as a better - derstanding of its internal structure, makes mathematical knowledge in many waysmore tractable than generalknowledge,as traditionally treatedin arti?cial intelligence. Similarly, we can also expect the problem of e?ectively using ma- ematical knowledge in automated ways to be much more tractable. This is the goal of the work in the cicm conferences and workshops. In the long view, so- ing the problems addressed by cicm is an important milestone in formulating the next generation of mathematical software.

• Coq
• accessible mathematics
• algorithmic theories
• automated deduction systems
• automated reasoning
• axiomatic theories
• code generation
• computational mathematics
• computational modeling
• computer algebra
• formal logic
• formal mathematics
• knowledge
• proving
• semantic web

• Department of Computing and Software, McMaster University, Hamilton, Canada

  Jacques Carette

• Informatics, 2.02 Informatics Forum, University of Edinburgh, Edinburgh, UK

  Lucas Dixon

• Department of Computer Science, University of Bologna, Bologna, Italy

  Claudio Sacerdoti Coen

• Department of Computer Science MC 375, University of Western Ontario, London, Canada

  Stephen M. Watt

Policies and ethics