×

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. (English) Zbl 1165.68005

Lecture Notes in Computer Science 5625. Lecture Notes in Artificial Intelligence. Berlin: Springer (ISBN 978-3-642-02613-3/pbk). xix, 493 p. (2009).

Show indexed articles as search result.

The articles of this volume will be reviewed individually. The preceding symposium Calculemus 2008 and the preceding conference MKM 2008 have been reviewed (see Zbl 1154.68002).
Indexed articles:
Arthan, Rob, Computational logic and continuous mathematics, pure and applied, 1 [Zbl 1243.68263]
Blostein, Dorothea, Math-literate computers, 2-13 [Zbl 1247.68226]
Calmet, Jacques, Abstraction-based information technology: a framework for open mechanized reasoning, 14-26 [Zbl 1247.68233]
Gonthier, Georges, Software engineering for mathematics, 27 [Zbl 1247.68235]
Ion, Patrick D. F., Some traditional mathematical knowledge management, 28 [Zbl 1247.68272]
Panic, Marko, Math handwriting recognition in Windows 7 and its benefits, 29-30 [Zbl 1247.68230]
Ruddy, David, Assembling the digital mathematics library, 31 [Zbl 1247.00054]
Fitch, John, CAMAL 40 years on – is small still beautiful?, 32-44 [Zbl 1247.68323]
Aranda-Corral, Gonzalo A.; Borrego-Díaz, Joaquín; Fernández-Lebrón, M. Magdalena, Conservative retractions of propositional logic theories by means of Boolean derivatives: theoretical foundations, 45-58 [Zbl 1247.03016]
Boldo, Sylvie; Filliâtre, Jean-Christophe; Melquiond, Guillaume, Combining Coq and Gappa for certifying floating-point programs, 59-74 [Zbl 1247.68232]
Bradford, Russell; Davenport, James H.; Sangwin, Christopher J., A comparison of equality in computer algebra and correctness in mathematical pedagogy, 75-89 [Zbl 1247.97004]
Kissinger, Aleks, Exploring a quantum theory with graph rewriting and computer algebra, 90-105 [Zbl 1247.68324]
Martín-Mateos, Francisco-Jesus; Rubio, Julio; Ruiz-Reina, Jose-Luis, ACL2 verification of simplicial degeneracy programs in the Kenzo system, 106-121 [Zbl 1247.68325]
Passmore, Grant Olney; Jackson, Paul B., Combined decision techniques for the existential theory of the reals, 122-137 [Zbl 1247.03018]
Sexton, Alan P.; Sorge, Volker; Watt, Stephen M., Reasoning with generic cases in the arithmetic of abstract matrices, 138-153 [Zbl 1247.68327]
Shemyakova, Ekaterina, Invariant properties of third-order non-hyperbolic linear partial differential operators, 154-169 [Zbl 1247.68328]
Tarau, Paul, A groupoid of isomorphic data transformations, 170-185 [Zbl 1247.68048]
Watt, Stephen M., Algorithms for the functional decomposition of Laurent polynomials, 186-200 [Zbl 1247.68329]
Baker, Josef B.; Sexton, Alan P.; Sorge, Volker, A linear grammar approach to mathematical formula recognition from PDF, 201-216 [Zbl 1247.68225]
Calude, Cristian S.; Müller, Christine, Formal proof: reconciling correctness and understanding, 217-232 [Zbl 1247.03017]
Carette, Jacques; Farmer, William M., A review of mathematical knowledge management, 233-246 [Zbl 1247.68266]
Collins, Joseph B., OpenMath content dictionaries for SI quantities and units, 247-262 [Zbl 1247.68267]
Davenport, James H.; Kohlhase, Michael, Unifying math ontologies: a tale of two standards, 263-278 [Zbl 1247.68268]
Giceva, Jana; Lange, Christoph; Rabe, Florian, Integrating web services into active mathematical documents, 279-293 [Zbl 1247.68314]
Goguadze, George, Representation for interactive exercises, 294-309 [Zbl 1247.97038]
Gozli, Davood G.; Pollanen, Marco; Reynolds, Michael, The characteristics of writing environments for mathematics: behavioral consequences and implications for software design and usability, 310-324 [Zbl 1247.68270]
Heeren, Bastiaan; Jeuring, Johan, Canonical forms in interactive exercise assistants, 325-340 [Zbl 1247.97039]
Kohlhase, Andrea; Kohlhase, Michael, Spreadsheet interaction with frames: exploring a mathematical practice, 341-356 [Zbl 1247.68274]
Kohlhase, Andrea; Kohlhase, Michael, Compensating the computational bias of spreadsheets with MKM techniques, 357-372 [Zbl 1247.68275]
Lamar, Robert; Kamareddine, Fairouz; Wells, J. B., MathLang translation to Isabelle syntax, 373-388 [Zbl 1247.68278]
Lange, Christoph; Kohlhase, Michael, A mathematical approach to ontology authoring and documentation, 389-404 [Zbl 1247.68279]
Mamane, Lionel Elie; Geuvers, Herman; McKinna, James, A logically saturated extension of \(\overline{\lambda}\mu\tilde{\mu}\), 405-421 [Zbl 1247.68239]
Jandhyala, Ramana C.; Krishnamoorthy, Mukkai; Nagy, George; Padmanabhan, Raghav; Seth, Sharad; Silversmith, William, From tessellations to table interpretation, 422-437 [Zbl 1247.68273]
Biha, Sidi Ould, Finite groups representation theory with Coq, 438-452 [Zbl 1247.68231]
Muhammad, Aslam; Martinez Enriquez, Ana Maria; Escalada-Imaz, Gonzalo, Collaborative assistant to handle MathML expressions, 453-459 [Zbl 1247.68283]
Golubitsky, Oleg; Watt, Stephen M., Confidence measures in recognizing handwritten mathematical symbols, 460-466 [Zbl 1247.68228]
Heras, Jónathan; Pascual, Vico; Rubio, Julio, Using open mathematical documents to interface computer algebra and proof assistant systems, 467-473 [Zbl 1247.68271]
Horn, Peter; Roozemond, Dan, OpenMath in SCIEnce: SCSCP and POPCORN, 474-479 [Zbl 1247.68316]
Rich, A. D.; Jeffrey, D. J., A knowledge repository for indefinite integration based on transformation rules, 480-485 [Zbl 1247.68326]
Sacerdoti Coen, Claudio; Tassi, Enrico, Natural deduction environment for Matita, 486-491 [Zbl 1247.68240]

MSC:

68-06 Proceedings, conferences, collections, etc. pertaining to computer science
68Txx Artificial intelligence
00B25 Proceedings of conferences of miscellaneous specific interest

Citations:

Zbl 1154.68002

Software:

ACL2; Coq
PDFBibTeX XMLCite
Full Text: DOI