Watt, Stephen M. (ed.); Davenport, James H. (ed.); Sexton, Alan P. (ed.); Sojka, Petr (ed.); Urban, Josef (ed.) 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] Cited in 1 ReviewCited in 7 Documents MSC: 68-06 Proceedings, conferences, collections, etc. pertaining to computer science 68Txx Artificial intelligence 00B25 Proceedings of conferences of miscellaneous specific interest Citations:Zbl 1268.68008 Software:HOL; HOL Light; Mizar; WolframAlpha; MathHub.info PDFBibTeX XMLCite \textit{S. M. Watt} (ed.) et al., Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7--11, 2014. Proceedings. Berlin: Springer (2014; Zbl 1293.68035) Full Text: DOI