Intelligent computer mathematics. 12th international conference, CICM 2019, Prague, Czech Republic, July 8–12, 2019. Proceedings. (English) Zbl 1428.68028

Lecture Notes in Computer Science 11617. Lecture Notes in Artificial Intelligence. Cham: Springer (ISBN 978-3-030-23249-8/pbk; 978-3-030-23250-4/ebook). xii, 307 p. (2019).

Show indexed articles as search result.

The articles of this volume will be reviewed individually. For the preceding conference see [Zbl 1392.68030].
Indexed articles:
Wenzel, Makarius, Interaction with formal mathematical documents in Isabelle/PIDE, 1-15 [Zbl 1428.68347]
Bayer, Jonas; David, Marco; Pal, Abhik; Stock, Benedikt, Beginners’ quest to formalize mathematics: a feasibility study in Isabelle, 16-27 [Zbl 1428.68340]
Berčič, Katja; Kohlhase, Michael; Rabe, Florian, Towards a unified mathematical data infrastructure: database and interface generation, 28-43 [Zbl 1428.68356]
Brown, Chad E.; Pąk, Karol, A tale of two set theories, 44-60 [Zbl 1428.68348]
Condoluci, Andrea; Kohlhase, Michael; Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio; Wenzel, Makarius, Relational data across mathematical libraries, 61-76 [Zbl 1428.68352]
Dundua, Besik; Kutsia, Temur; Marin, Mircea, Variadic equational matching, 77-92 [Zbl 1428.68341]
England, Matthew; Florescu, Dorian, Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition, 93-108 [Zbl 1428.68399]
Carette, Jacques; Farmer, William M., Towards specifying symbolic computation, 109-124 [Zbl 1428.68397]
Johansson, Moa, Lemma discovery for induction. A survey, 125-139 [Zbl 1428.68342]
Kovács, Zoltán; Pech, Pavel, Experiments on automatic inclusion of some non-degeneracy conditions among the hypotheses in locus equation computations, 140-154 [Zbl 1428.68343]
Maletzky, Alexander, Formalization of Dubé’s degree bounds for Gröbner bases in Isabelle/HOL, 155-170 [Zbl 1428.68349]
Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio, The Coq library as a theory graph, 171-186 [Zbl 1428.68344]
Quinlan, Dee; Wells, Joe B.; Kamareddine, Fairouz, BNF-style notation as it is actually used, 187-204 [Zbl 1428.68350]
Rabe, Florian, MMTTeX: connecting content and narration-oriented document formats, 205-210 [Zbl 1428.68351]
Rabe, Florian; Sharoda, Yasmine, Diagram combinators in MMT, 211-226 [Zbl 1428.68353]
Raggi, Daniel; Stockdill, Aaron; Jamnik, Mateja; Garcia Garcia, Grecia; Sutherland, Holly E. A.; Cheng, Peter C.-H., Inspection and selection of representations, 227-242 [Zbl 1428.68293]
Sacerdoti Coen, Claudio, A plugin to export Coq libraries to XML, 243-257 [Zbl 1428.68345]
Schubotz, Moritz; Teschke, Olaf; Stange, Vincent; Meuschke, Norman; Gipp, Bela, Forms of plagiarism in digital mathematical libraries, 258-274 [Zbl 1428.68358]
Amann, Kai; Kohlhase, Michael; Rabe, Florian; Wiesing, Tom, Integrating semantic mathematical documents and dynamic notebooks, 275-290 [Zbl 1428.68355]
Youssef, Abdou; Miller, Bruce R., Explorations into the use of word embedding in math search and math semantics, 291-305 [Zbl 1428.68354]

MSC:

68-06	Proceedings, conferences, collections, etc. pertaining to computer science
68Txx	Artificial intelligence
68Vxx	Computer science support for mathematical research and practice
00B25	Proceedings of conferences of miscellaneous specific interest

Citations:

Zbl 1392.68030

Software:

MMTTeX; MMT; Isabelle/PIDE; Coq; Isabelle/HOL; Isabelle