Intelligent Computer Mathematics [[electronic resource] ] : 12th International Conference, CICM 2019, Prague, Czech Republic, July 8–12, 2019, Proceedings / / edited by Cezary Kaliszyk, Edwin Brady, Andrea Kohlhase, Claudio Sacerdoti Coen
| Intelligent Computer Mathematics [[electronic resource] ] : 12th International Conference, CICM 2019, Prague, Czech Republic, July 8–12, 2019, Proceedings / / edited by Cezary Kaliszyk, Edwin Brady, Andrea Kohlhase, Claudio Sacerdoti Coen |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (XII, 307 p. 540 illus., 70 illus. in color.) |
| Disciplina | 004.0151 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Computers Artificial Intelligence Theory of Computation Information Systems and Communication Service |
| ISBN | 3-030-23250-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Interaction 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. |
| Record Nr. | UNISA-996465578503316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Intelligent Computer Mathematics : 12th International Conference, CICM 2019, Prague, Czech Republic, July 8–12, 2019, Proceedings / / edited by Cezary Kaliszyk, Edwin Brady, Andrea Kohlhase, Claudio Sacerdoti Coen
| Intelligent Computer Mathematics : 12th International Conference, CICM 2019, Prague, Czech Republic, July 8–12, 2019, Proceedings / / edited by Cezary Kaliszyk, Edwin Brady, Andrea Kohlhase, Claudio Sacerdoti Coen |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (XII, 307 p. 540 illus., 70 illus. in color.) |
| Disciplina | 004.0151 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Computer science Computer networks Artificial Intelligence Theory of Computation Computer Communication Networks |
| ISBN | 3-030-23250-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Interaction 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. |
| Record Nr. | UNINA-9910349315803321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Intelligent Computer Mathematics [[electronic resource] ] : International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings. / / edited by Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, Volker Sorge
| Intelligent Computer Mathematics [[electronic resource] ] : International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings. / / edited by Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, Volker Sorge |
| Edizione | [1st ed. 2015.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 |
| Descrizione fisica | 1 online resource (XXI, 359 p. 84 illus.) |
| Disciplina | 006.30151 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Computer science—Mathematics
Artificial intelligence Mathematical logic Natural language processing (Computer science) Information storage and retrieval Math Applications in Computer Science Artificial Intelligence Symbolic and Algebraic Manipulation Mathematical Logic and Formal Languages Natural Language Processing (NLP) Information Storage and Retrieval |
| ISBN | 3-319-20615-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Calculemus -- Digital Mathematics Libraries -- Mathematical Knowledge Management -- Projects and Surveys -- Systems and Data. |
| Record Nr. | UNISA-996198514103316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Intelligent Computer Mathematics : International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings. / / edited by Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, Volker Sorge
| Intelligent Computer Mathematics : International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings. / / edited by Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, Volker Sorge |
| Edizione | [1st ed. 2015.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 |
| Descrizione fisica | 1 online resource (XXI, 359 p. 84 illus.) |
| Disciplina | 006.30151 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Computer science - Mathematics
Artificial intelligence Machine theory Natural language processing (Computer science) Information storage and retrieval systems Mathematical Applications in Computer Science Artificial Intelligence Symbolic and Algebraic Manipulation Formal Languages and Automata Theory Natural Language Processing (NLP) Information Storage and Retrieval |
| ISBN | 3-319-20615-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Calculemus -- Digital Mathematics Libraries -- Mathematical Knowledge Management -- Projects and Surveys -- Systems and Data. |
| Record Nr. | UNINA-9910484373003321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Lo trovi qui: Univ. Federico II | ||
| ||