000898725 000__ 04321cam\a2200541Ii\4500 000898725 001__ 898725 000898725 005__ 20230306150240.0 000898725 006__ m\\\\\o\\d\\\\\\\\ 000898725 007__ cr\cn\nnnunnun 000898725 008__ 190712s2019\\\\sz\\\\\\o\\\\\101\0\eng\d 000898725 019__ $$a1110229363$$a1110939930$$a1111682840$$a1112124667$$a1112472392 000898725 020__ $$a9783030232504$$q(electronic book) 000898725 020__ $$a3030232506$$q(electronic book) 000898725 020__ $$z3030232492 000898725 020__ $$z9783030232498 000898725 0248_ $$a10.1007/978-3-030-23 000898725 035__ $$aSP(OCoLC)on1107874685 000898725 035__ $$aSP(OCoLC)1107874685$$z(OCoLC)1110229363$$z(OCoLC)1110939930$$z(OCoLC)1111682840$$z(OCoLC)1112124667$$z(OCoLC)1112472392 000898725 040__ $$aYDX$$beng$$erda$$cYDX$$dYDXIT$$dLQU$$dGW5XE$$dOCLCF$$dUKMGB 000898725 049__ $$aISEA 000898725 050_4 $$aQA76.9.M35$$bC53 2019 000898725 08204 $$a004.01/51$$223 000898725 1112_ $$aCICM (Conference)$$n(12th :$$d2019 :$$cPrague, Czech Republic) 000898725 24510 $$aIntelligent computer mathematics :$$b12th international conference, CICM 2019, Prague, Czech Republic, July 8-12, 2019, Proceedings /$$cCezary Kaliszyk [and 3 others] (eds.). 000898725 2463_ $$aCICM 2019 000898725 264_1 $$aCham, Switzerland :$$bSpringer,$$c[2019] 000898725 300__ $$a1 online resource. 000898725 336__ $$atext$$btxt$$2rdacontent 000898725 337__ $$acomputer$$bc$$2rdamedia 000898725 338__ $$aonline resource$$bcr$$2rdacarrier 000898725 4901_ $$aLecture notes in artificial intelligence ;$$v11617 000898725 4901_ $$aLNCS sublibrary. SL 7, Artificial intelligence 000898725 500__ $$aIncludes author index. 000898725 5050_ $$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. 000898725 506__ $$aAccess limited to authorized users. 000898725 520__ $$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. 000898725 588__ $$aDescription based on online resource; title from digital title page (viewed on July 26, 2019). 000898725 650_0 $$aComputer science$$xMathematics$$vCongresses. 000898725 650_0 $$aArtificial intelligence$$xMathematics$$vCongresses. 000898725 7001_ $$aKaliszyk, Cezary,$$eeditor. 000898725 77608 $$iPrint version: $$z3030232492$$z9783030232498$$w(OCoLC)1101971458 000898725 830_0 $$aLecture notes in computer science ;$$v11617. 000898725 830_0 $$aLecture notes in computer science.$$pLecture notes in artificial intelligence. 000898725 830_0 $$aLNCS sublibrary.$$nSL 7,$$pArtificial intelligence. 000898725 852__ $$bebk 000898725 85640 $$3SpringerLink$$uhttps://univsouthin.idm.oclc.org/login?url=http://link.springer.com/10.1007/978-3-030-23250-4$$zOnline Access$$91397441.1 000898725 909CO $$ooai:library.usi.edu:898725$$pGLOBAL_SET 000898725 980__ $$aEBOOK 000898725 980__ $$aBIB 000898725 982__ $$aEbook 000898725 983__ $$aOnline 000898725 994__ $$a92$$bISE