| Contents |
Computational logic and continuous mathematics, pure and applied / Rob Arthan -- Math-literate computers / Dorothea Blostein -- Abstraction-based information technology: a framework for open mechanized reasoning / Jacques Calmet -- Software engineering for mathematics / Georges Gonthier -- Some traditional mathematical knowledge management / Patrick D.F. Ion -- Math handwriting recognition in windows 7 and its benefits / Marko Panic -- Assembling the digital mathematics library / David Ruddy -- CAMAL 40 years on -- is small still beautiful? / John Fitch -- Conservative retractions of propositional logic theories by means of Boolean derivatives: theoretical foundations / Gonzalo A. Aranda-Corral, Joaquin Borrego-Diaz, and M. Magdalena Fernandez-Lebron -- Combining Coq and Gappa for certifying floating-point programs / Sylvie Boldo, Jean-Christophe Filliatre, and Guillaume Melquiond -- A comparison of equality in computer algebra and correctness in mathematical pedagogy / Russell Bradford, James H. Davenport, and Christopher J. Sangwin -- Exploring a quantum theory with graph rewriting and computer algebra / Aleks Kissinger -- ACL2 verification of simplicial degeneracy programs in the kenzo system / Francisco-Jesus Martin-Mateos, Julio Rubio, and Jose-Luis Ruiz-Reina -- Combined decision techniques for the existential theory of the reals / Grant Olney Passmore and Paul B. Jackson -- Reasoning with generic cases in the arithmetic of abstract matrices / Alan P. Sexton, Volker Sorge, and Stephen M. Watt -- Invariant Properties of third-order non-hyperbolic linear partial differential operators / Ekaterina Shemyakova -- A grooupoid of isomorphic data transformations / Paul Tarau -- Algorithms for the functional decomposition of Laurent polynomials / Stephen M. Watt -- A linear grammar approach to mathematical formula recognition from PDF / Josef B. Baker, Alan P. Sexton, and Volker Sorge -- Formal proof: reconciling correctness and understanding / Cristian S. Calude and Christine Muller -- A review of mathematical knowledge management / Jacques Carette and William M. Farmer -- OpenMath content dictionaries for SI quantities and units / Joseph B. Collins -- Unifying math ontologies: a tale of two standards / James H. Davenport and Michael Kohlhase -- Integrating web services into active mathematical documents / Jana Giceva, Christoph Lange, and Florian Rabe -- Representation for interactive exercises / George Goguadze -- The characteristics of writing environments for mathematics: behavioral consequences and implications for software design and usability / Davood G. Gozli, Marco Pollanen, and Michael Reynolds -- Canonical forms in interactive exercises assistants / Bastiaan Heeren and Johan Jeuring -- Spreadsheet interaction with frames: exploring a mathematical practice / Andrea Kohlhase and Michael Kohlhase -- Compensating the computational bias of spreadsheets with MKM techniques / Andrea Kohlhase and Michael Kohlhase -- Mathlang translation to Isabelle Syntax / Robert Lamar, Fairouz Kamareddine, and J.B. Wells -- A mathematical approach to ontology authoring and documentation / Christoph Lange and Michael Kohlhase -- A logically saturated extension of / Lionel Elie Mamane, Herman Geuvers, and James McKinna -- From tessellations to table interpretation / Ramana C. Jandhyala [and others] -- Finite groups representation theory with coq / Sidi Ould Biha -- Collaborative assistant to handle mathML expressions / Aslam Muhammad, Ana Maria Martinez Enriquez, and Gonzalo Escalada-Imaz -- Confidence measures in recognizing handwritten mathematical symbols / Oleg Golubitsky and Stephen M. Watt -- Using open mathematical documents to interface computer algebra and proof assistant systems / Jonathan Heras, Vico Pascual, and Julio Rubio -- OpenMath in SCIEnce: SCSCP and POPCORN / Peter Horn and Dan Roozemond -- A knowledge repository for indefinite integration based on transformation rules / A.D. Rich and D.J. Jeffrey -- Natural deduction environment for matita / Claudio Sacerdoti Coen and Enrico Tassi. |
