×

zbMATH — the first resource for mathematics

Intelligent computer mathematics. MKM, Calculemus, DML, and systems and projects 2013, held as part of CICM 2013, Bath, UK, July 8–12, 2013. Proceedings. (English) Zbl 1268.68008
Lecture Notes in Computer Science 7961. Lecture Notes in Artificial Intelligence. Berlin: Springer (ISBN 978-3-642-39319-8/pbk). xv, 384 p. (2013).

Show indexed articles as search result.

The articles of this volume will be reviewed individually. For the preceding conference see [Zbl 1245.68013].
Indexed articles:
Mahboubi, Assia, The rooster and the butterflies, 1-18 [Zbl 1390.68581]
Bradford, Russell; Davenport, James H.; England, Matthew; Wilson, David, Optimising problem formulation for cylindrical algebraic decomposition, 19-34 [Zbl 1390.68775]
Farmer, William M., The formalization of syntax-based mathematical algorithms using quotation and evaluation, 35-50 [Zbl 1390.68778]
Allamigeon, Xavier; Gaubert, Stéphane; Magron, Victor; Werner, Benjamin, Certification of bounds of non-linear functions: the templates method, 51-65 [Zbl 1390.68570]
Kohlhase, Michael; Mance, Felix; Rabe, Florian, A universal machine for biform theory graphs, 82-97 [Zbl 1278.68267]
Martin, Ursula; Pease, Alison, Mathematical practice, crowdsourcing, and social machines, 98-119 [Zbl 1390.01101]
Kaliszyk, Cezary; Urban, Josef, Automated reasoning service for HOL Light, 120-135 [Zbl 1390.68576]
England, Matthew; Bradford, Russell; Davenport, James H.; Wilson, David, Understanding branch cuts of expressions, 136-151 [Zbl 1390.68777]
Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman, Formal mathematics on display: a wiki for Flyspeck, 152-167 [Zbl 1390.68751]
Hu, Rui; Watt, Stephen M., Determining points on handwritten mathematical symbols, 168-183 [Zbl 1390.68566]
Obua, Steven; Adams, Mark; Aspinall, David, Capturing hiproofs in HOL light, 184-199 [Zbl 1390.68583]
Lange, Christoph; Caminati, Marco B.; Kerber, Manfred; Mossakowski, Till; Rowat, Colin; Wenzel, Makarius; Windsteiger, Wolfgang, A qualitative comparison of the suitability of four theorem provers for basic auction theory, 200-215 [Zbl 1390.68577]
Tonisson, Eno, Students’ comparison of their trigonometric answers with the answers of a computer algebra system, 216-229 [Zbl 1390.97003]
Ion, Patrick D. F., Mathematics and the World Wide Web, 230-245 [Zbl 1390.01100]
Kamali, Shahab; Tompa, Frank Wm., Structural similarity search for mathematics retrieval, 246-262 [Zbl 1390.68258]
Růžička, Michal; Sojka, Petr; Krejčíř, Vlastimil, Towards machine-actionable modules of a digital mathematics library. The example of DML-CZ, 263-277 [Zbl 1353.68290]
Nghiem, Minh-Quoc; Kristianto, Giovanni Yoko; Topić, Goran; Aizawa, Akiko, A hybrid approach for semantic enrichment of MathML mathematical expressions, 278-287 [Zbl 1353.68289]
Miller, Bruce R., Three years of DLMF: web, math and search, 288-295 [Zbl 1390.68750]
Libbrecht, Paul, Escaping the trap of too precise topic queries, 296-309 [Zbl 1390.68749]
Do, Chau; Pauwels, Eric J., Using MathML to represent units of measurement for improved ontology alignment, 310-325 [Zbl 1390.68619]
Lüth, Christoph; Ring, Martin, A web interface for Isabelle: the next generation, 326-329 [Zbl 1390.68580]
Lange, Christoph; Rowat, Colin; Kerber, Manfred, The ForMaRE project – formal mathematical reasoning in economics, 330-334 [Zbl 1390.68578]
Ginev, Deyan; Miller, Bruce R., LaTeXml 2012 – a year of LaTeXml, 335-338 [Zbl 1390.68740]
Rabe, Florian, The MMT API: a generic MKM system, 339-343 [Zbl 1390.68626]
Chebukov, Dmitry E.; Izaak, Alexander D.; Misyurina, Olga G.; Pupyrev, Yuri A.; Zhizhchenko, Alexey B., Math-Net.Ru as a digital archive of the Russian mathematical knowledge from the XIX century to today, 344-348 [Zbl 1390.68748]
Abánades, Miguel A.; Botana, Francisco, A dynamic symbolic geometry environment based on the GröbnerCover algorithm for the computation of geometric loci and envelopes, 349-353 [Zbl 1390.68774]
Heras, Jónathan; Komendantskaya, Ekaterina, ML4PG in computer algebra verification, 354-358 [Zbl 1390.68780]
Barras, Bruno; del Carmen González Huesca, Lourdes; Herbelin, Hugo; Régis-Gianas, Yann; Tassi, Enrico; Wenzel, Makarius; Wolff, Burkhart, Pervasive parallelism in highly-trustable interactive theorem proving systems, 359-363 [Zbl 1390.68571]
Quaresma, Pedro; Santos, Vanda; Bouallegue, Seifeddine, The web geometry laboratory project, 364-368 [Zbl 1390.97006]
Bönisch, Sebastian; Brickenstein, Michael; Chrapary, Hagen; Greuel, Gert-Martin; Sperber, Wolfram, swMATH – a new information service for mathematical software, 369-373 [Zbl 1272.68451]
Prank, Rein, Software for evaluating relevance of steps in algebraic transformations, 374-378 [Zbl 1390.97007]
Schöneberg, Ulf; Sperber, Wolfram, The DeLiVerMath project. Text analysis in mathematics, 379-382 [Zbl 1270.68363]
Reviewer: Reviewer (Berlin)

MSC:
68-06 Proceedings, conferences, collections, etc. pertaining to computer science
68Txx Artificial intelligence
00B25 Proceedings of conferences of miscellaneous specific interest
Software:
HOL Light; MMT
PDF BibTeX XML Cite
Full Text: DOI