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


Zbl 1268.68008
Full Text: DOI