zbMATH — the first resource for mathematics

Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings. (English) Zbl 1293.68035
Lecture Notes in Computer Science 8543. Lecture Notes in Artificial Intelligence. Berlin: Springer (ISBN 978-3-319-08433-6/pbk). xx, 458 p. (2014).

Show indexed articles as search result.

The articles of this volume will be reviewed individually. For the preceding conference see [Zbl 1268.68008].
Indexed articles:
Weisstein, Eric, Computable data, mathematics, and digital libraries in Mathematica and Wolfram\(|\)Alpha, 26-29 [Zbl 1304.68202]
Ahmed, Waqar; Hasan, Osman; Tahar, Sofiene; Hamdi, Mohammad Salah, Towards the formal reliability analysis of oil and gas pipelines, 30-44 [Zbl 1304.68151]
England, Matthew; Bradford, Russell; Chen, Changbo; Davenport, James H.; Maza, Marc Moreno; Wilson, David, Problem formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition, 45-60 [Zbl 1304.68223]
Cerna, David, A tableaux-based decision procedure for multi-parameter propositional schemata, 61-75 [Zbl 1304.03044]
Fish, Andrew; Lisitsa, Alexei, Detecting unknots via equational reasoning. I: Exploration, 76-91 [Zbl 1304.68153]
Huang, Zongyan; England, Matthew; Wilson, David; Davenport, James H.; Paulson, Lawrence C.; Bridge, James, Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition, 92-107 [Zbl 1304.68224]
Johansson, Moa; Rosén, Dan; Smallbone, Nicholas; Claessen, Koen, Hipster: integrating theory exploration in a proof assistant, 108-122 [Zbl 1304.68157]
Afshar, Sanaz Khan; Aravantinos, Vincent; Hasan, Osman; Tahar, Sofiène, Formalization of complex vectors in higher-order logic, 123-137 [Zbl 1304.68150]
Wegner, Bernd; Schindler, Sigram, A mathematical structure for modeling inventions, 138-152 [Zbl 1304.68201]
Kohlhase, Andrea, Search interfaces for mathematicians, 153-168 [Zbl 1304.68198]
Kohlhase, Michael, A data model and encoding for a semantic, multilingual terminology of mathematics, 169-183 [Zbl 1304.68173]
Moore, Ross, PDF/A-3u as an archival format for accessible mathematics, 184-199 [Zbl 1304.68174]
Nghiem, Minh-Quoc; Kristianto, Giovanni Yoko; Topić, Goran; Aizawa, Akiko, Which one is better: presentation-based or content-based math search?, 200-212 [Zbl 1304.68039]
Schöneberg, Ulf; Sperber, Wolfram, POS tagging and its applications for mathematics. Text analysis in mathematics, 213-223 [Zbl 1304.68180]
Schubotz, Moritz; Wicke, Gabriel, Mathoid: robust, scalable, fast and accessible math rendering for Wikipedia, 224-235 [Zbl 1304.68200]
Caminati, Marco B.; Kerber, Manfred; Lange, Christoph; Rowat, Colin, Set theory or higher order logic to represent auction concepts in Isabelle?, 236-251 [Zbl 1304.68152]
Carette, Jacques; Farmer, William M.; Kohlhase, Michael, Realms: a structure for consolidating knowledge about mathematical theories, 252-266 [Zbl 1304.68169]
Gauthier, Thibault; Kaliszyk, Cezary, Matching concepts across HOL libraries, 267-281 [Zbl 1304.68154]
Gransden, Thomas; Walkinshaw, Neil; Raman, Rajeev, Mining state-based models from proof corpora, 282-297 [Zbl 1304.68155]
Haralambous, Yannis; Quaresma, Pedro, Querying geometric figures using a controlled language, ontological graphs and dependency lattices, 298-311 [Zbl 1304.68170]
Horozal, Fulya; Rabe, Florian; Kohlhase, Michael, Flexary operators for formalized mathematics, 312-327 [Zbl 1304.68171]
Hupel, Lars, Interactive simplifier tracing and debugging in Isabelle, 328-343 [Zbl 1304.68156]
Jucovschi, Constantin, Towards an interaction-based integration of MKM services into end-user applications, 344-356 [Zbl 1304.68197]
Kaliszyk, Cezary; Rabe, Florian, Towards knowledge management for HOL Light, 357-372 [Zbl 1304.68158]
Pąk, Karol, Automated improving of proof legibility in the Mizar system, 373-387 [Zbl 1304.68160]
Stojanović, Sana; Narboux, Julien; Bezem, Marc; Janičić, Predrag, A vernacular for coherent logic, 388-403 [Zbl 1304.68163]
Zhang, Qun; Youssef, Abdou, An approach to math-similarity search, 404-418 [Zbl 1304.68040]
Cohl, Howard S.; McClain, Marjorie A.; Saunders, Bonita V.; Schubotz, Moritz; Williams, Janelle C., Digital repository of mathematical formulae, 419-422 [Zbl 1304.68194]
Ginev, Deyan; Corneli, Joseph, NNexus reloaded, 423-426 [Zbl 1304.68195]
Iancu, Mihnea; Jucovschi, Constantin; Kohlhase, Michael; Wiesing, Tom, System description: MathHub.info, 431-434 [Zbl 1304.68196]
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří; Geuvers, Herman, Developing corpus-based translation methods between informal and formal mathematics: project description, 435-439 [Zbl 1304.68172]
Kohlhase, Lukas; Kohlhase, Michael, System description: a semantics-aware LaTeX-to-office converter, 440-443 [Zbl 1304.68193]
Líška, Martin; Sojka, Petr; Růžička, Michal, Math indexer and searcher web interface. Towards fulfillment of mathematicians’ information needs, 444-448 [Zbl 1304.68199]
Naumowicz, Adam, SAT-enhanced Mizar proof checking, 449-452 [Zbl 1304.68159]
Siddique, Umair; Tahar, Sofiène, A framework for formal reasoning about geometrical optics, 453-456 [Zbl 1304.68162]

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