LEADER 04464nam 22005895 450 001 996465578503316 005 20200703221444.0 010 $a3-030-23250-6 024 7 $a10.1007/978-3-030-23250-4 035 $a(CKB)4100000008527455 035 $a(DE-He213)978-3-030-23250-4 035 $a(MiAaPQ)EBC5927996 035 $a(PPN)238488225 035 $a(EXLCZ)994100000008527455 100 $a20190702d2019 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aIntelligent Computer Mathematics$b[electronic resource] $e12th International Conference, CICM 2019, Prague, Czech Republic, July 8?12, 2019, Proceedings /$fedited by Cezary Kaliszyk, Edwin Brady, Andrea Kohlhase, Claudio Sacerdoti Coen 205 $a1st ed. 2019. 210 1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2019. 215 $a1 online resource (XII, 307 p. 540 illus., 70 illus. in color.) 225 1 $aLecture Notes in Artificial Intelligence ;$v11617 311 $a3-030-23249-2 320 $aIncludes bibliographical references and index. 327 $aInteraction with Formal Mathematical Documents in Isabelle/PIDE -- Beginners? quest to formalize mathematics: A feasibility study in Isabelle 16 -- Towards a Unified Mathematical Data Infrastructure: Database and Interface Generation -- A Tale of Two Set Theories -- Relational Data Across Mathematical Libraries -- Variadic Equational Matching -- Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition -- Towards Specifying Symbolic Computation -- Lemma Discovery for Induction - A survey -- Experiments on automatic inclusion of some non-degeneracy conditions among the hypotheses in locus equation computations -- Formalization of Dubé?s Degree Bounds for Gröbner Bases in Isabelle/HOL 155 -- Le Coq Library as a Theory Graph -- BNF-Style Notation as it is Actually Used -- MMTTeX: Connecting Content and Narration-Oriented Document Formats -- Diagram Combinators in MMT -- Inspection and selection of representations -- A plugin to export Coq libraries to XML -- Forms of Plagiarism in Digital Mathematical Libraries -- Integrating Semantic Mathematical Documents and Dynamic Notebooks -- Explorations into the Use of Word Embedding in Math Search and Math Semantics. 330 $aThis book constitutes the refereed proceedings of the 12th International Conference on Intelligent Computer Mathematics, CICM 2019, held in Prague, Czech Republic, in July 2019. The 19 full papers presented were carefully reviewed and selected from a total of 41 submissions. The papers focus on digital and computational solutions which are becoming the prevalent means for the generation, communication, processing, storage and curation of mathematical information. Separate communities have developed to investigate and build computer based systems for computer algebra, automated deduction, and mathematical publishing as well as novel user interfaces. While all of these systems excel in their own right, their integration can lead to synergies offering significant added value. 410 0$aLecture Notes in Artificial Intelligence ;$v11617 606 $aArtificial intelligence 606 $aComputers 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 606 $aTheory of Computation$3https://scigraph.springernature.com/ontologies/product-market-codes/I16005 606 $aInformation Systems and Communication Service$3https://scigraph.springernature.com/ontologies/product-market-codes/I18008 615 0$aArtificial intelligence. 615 0$aComputers. 615 14$aArtificial Intelligence. 615 24$aTheory of Computation. 615 24$aInformation Systems and Communication Service. 676 $a004.0151 702 $aKaliszyk$b Cezary$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aBrady$b Edwin$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aKohlhase$b Andrea$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aSacerdoti Coen$b Claudio$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996465578503316 996 $aIntelligent Computer Mathematics$92149623 997 $aUNISA