8. MKM / 16. Calculemus 2009:
Grand Bend,
Canada
Jacques Carette, Lucas Dixon, Claudio Sacerdoti Coen, Stephen M. Watt (Eds.):
Intelligent Computer Mathematics, 16th Symposium, Calculemus 2009, 8th International Conference, MKM 2009, Held as Part of CICM 2009, Grand Bend, Canada, July 6-12, 2009. Proceedings.
Lecture Notes in Computer Science 5625 Springer 2009, ISBN 978-3-642-02613-3
Joint Invited Talks
- Rob Arthan:
Computational Logic and Continuous Mathematics, Pure and Applied.
1
- Dorothea Blostein:
Math-Literate Computers.
2-13
- Jacques Calmet:
Abstraction-Based Information Technology: A Framework for Open Mechanized Reasoning.
14-26
- Georges Gonthier:
Software Engineering for Mathematics.
27
Calculemus Talks
- Patrick D. F. Ion:
Some Traditional Mathematical Knowledge Management.
28
- Marko Panic:
Math Handwriting Recognition in Windows 7 and Its Benefits.
29-30
- David Ruddy:
Assembling the Digital Mathematics Library.
31
- John Fitch:
CAMAL 40 Years on - Is Small Still Beautiful?.
32-44
- Gonzalo A. Aranda-Corral, Joaquín Borrego-Díaz, M. Magdalena Fernández-Lebrón:
Conservative Retractions of Propositional Logic Theories by Means of Boolean Derivatives: Theoretical Foundations.
45-58
- Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond:
Combining Coq and Gappa for Certifying Floating-Point Programs.
59-74
- Russell J. Bradford, James H. Davenport, Christopher J. Sangwin:
A Comparison of Equality in Computer Algebra and Correctness in Mathematical Pedagogy.
75-89
- Aleks Kissinger:
Exploring a Quantum Theory with Graph Rewriting and Computer Algebra.
90-105
- Francisco-Jesús Martín-Mateos, Julio Rubio, José-Luis Ruiz-Reina:
ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System.
106-121
- Grant Olney Passmore, Paul B. Jackson:
Combined Decision Techniques for the Existential Theory of the Reals.
122-137
- Alan P. Sexton, Volker Sorge, Stephen M. Watt:
Reasoning with Generic Cases in the Arithmetic of Abstract Matrices.
138-153
- Ekaterina Shemyakova:
Invariant Properties of Third-Order Non-hyperbolic Linear Partial Differential Operators.
154-169
- Paul Tarau:
A Groupoid of Isomorphic Data Transformations.
170-185
- Stephen M. Watt:
Algorithms for the Functional Decomposition of Laurent Polynomials.
186-200
MKM Talks
- Josef B. Baker, Alan P. Sexton, Volker Sorge:
A Linear Grammar Approach to Mathematical Formula Recognition from PDF.
201-216
- Cristian S. Calude, Christine Müller:
Formal Proof: Reconciling Correctness and Understanding.
217-232
- Jacques Carette, William M. Farmer:
A Review of Mathematical Knowledge Management.
233-246
- Joseph B. Collins:
OpenMath Content Dictionaries for SI Quantities and Units.
247-262
- James H. Davenport, Michael Kohlhase:
Unifying Math Ontologies: A Tale of Two Standards.
263-278
- Jana Giceva, Christoph Lange, Florian Rabe:
Integrating Web Services into Active Mathematical Documents.
279-293
- George Goguadze:
Representation for Interactive Exercises.
294-309
- Davood G. Gozli, Marco Pollanen, Michael Reynolds:
The Characteristics of Writing Environments for Mathematics: Behavioral Consequences and Implications for Software Design and Usability.
310-324
- Bastiaan Heeren, Johan Jeuring:
Canonical Forms in Interactive Exercise Assistants.
325-340
- Andrea Kohlhase, Michael Kohlhase:
Spreadsheet Interaction with Frames: Exploring a Mathematical Practice.
341-356
- Andrea Kohlhase, Michael Kohlhase:
Compensating the Computational Bias of Spreadsheets with MKM Techniques.
357-372
- Robert Lamar, Fairouz Kamareddine, J. B. Wells:
MathLang Translation to Isabelle Syntax.
373-388
- Christoph Lange, Michael Kohlhase:
A Mathematical Approach to Ontology Authoring and Documentation.
389-404
- Lionel Elie Mamane, Herman Geuvers, James McKinna:
A Logically Saturated Extension of .
405-421
- Ramana C. Jandhyala, Mukkai S. Krishnamoorthy, George Nagy, Raghav K. Padmanabhan, Sharad C. Seth, William Silversmith:
From Tessellations to Table Interpretation.
422-437
- Sidi Ould Biha:
Finite Groups Representation Theory with Coq.
438-452
- Aslam Muhammad, Ana María Martínez Enríquez, Gonzalo Escalada-Imaz:
Collaborative Assistant to Handle MathML Expressions.
453-459
- Oleg Golubitsky, Stephen M. Watt:
Confidence Measures in Recognizing Handwritten Mathematical Symbols.
460-466
- Jónathan Heras, Vico Pascual, Julio Rubio:
Using Open Mathematical Documents to Interface Computer Algebra and Proof Assistant Systems.
467-473
- Peter Horn, Dan Roozemond:
OpenMath in SCIEnce: SCSCP and POPCORN.
474-479
- A. D. Rich, David J. Jeffrey:
A Knowledge Repository for Indefinite Integration Based on Transformation Rules.
480-485
- Claudio Sacerdoti Coen, Enrico Tassi:
Natural Deduction Environment for Matita.
486-491
Copyright © Wed Nov 25 18:59:51 2009
by Michael Ley (ley@uni-trier.de)