LEADER 07372nam 22008055 450 001 9910484944603321 005 20200629120258.0 010 $a3-319-08434-8 024 7 $a10.1007/978-3-319-08434-3 035 $a(CKB)3710000000143885 035 $a(SSID)ssj0001276165 035 $a(PQKBManifestationID)11836025 035 $a(PQKBTitleCode)TC0001276165 035 $a(PQKBWorkID)11239049 035 $a(PQKB)10530348 035 $a(DE-He213)978-3-319-08434-3 035 $a(MiAaPQ)EBC3093097 035 $a(PPN)179766538 035 $a(EXLCZ)993710000000143885 100 $a20140630d2014 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aIntelligent Computer Mathematics $eCICM 2014 Joint Events: Calculemus, DML, MKM, and Systems and Projects 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings /$fedited by Stephen M. Watt, Alan Sexton, James H. Davenport, Petr Sojka, Josef Urban 205 $a1st ed. 2014. 210 1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2014. 215 $a1 online resource (XX, 458 p. 111 illus.) 225 1 $aLecture Notes in Artificial Intelligence ;$v8543 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-319-08433-X 327 $aInvited Talks.-What International Studies Say about the Importance and Limitations of Using Computers to Teach Mathematics in Secondary Schools -- Towards Robust Hyperlinks for Web-Based Scholarly Communication -- Computable Data, Mathematics, and Digital Libraries in Mathematica and Wolfram Alpha -- Calculemus -- Towards the Formal Reliability Analysis of Oil and Gas Pipelines -- Problem Formulation for Truth-Table Invariant Cylindrical Algebraic Decomposition by Incremental Triangular Decomposition -- A Tableaux-Based Decision Procedure for Multi-parameter Propositional Schemata -- Detecting Unknots via Equational Reasoning, I: Exploration -- Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition -- Hipster: Integrating Theory Exploration in a Proof Assistant -- Formalization of Complex Vectors in Higher-Order Logic -- A Mathematical Structure for Modeling Inventions -- Digital Mathematics Library -- Search Interfaces for Mathematicians -- A Data Model and Encoding for a Semantic, Multilingual Terminology of Mathematics -- PDF/A-3u as an Archival Format for Accessible Mathematics -- Which One Is Better: Presentation-Based or Content-Based Math Search? -- POS Tagging and Its Applications for Mathematics -- Mathoid: Robust, Scalable, Fast and Accessible Math Rendering for Wikipedia -- Mathematical Knowledge Management -- Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle? -- Realms: A Structure for Consolidating Knowledge about Mathematical Theories -- Matching Concepts across HOL Libraries -- Mining State-Based Models from Proof Corpora -- Querying Geometric Figures Using a Controlled Language, Ontological Graphs and Dependency Lattices -- Flexary Operators for Formalized Mathematics -- Interactive Simplifier Tracing and Debugging in Isabelle -- Towards an Interaction-based Integration of MKM Services into End-User Applications -- Towards Knowledge Management for HOL Light -- Automated Improving of Proof Legibility in the Mizar System -- A Vernacular for Coherent Logic -- An Approach to Math-Similarity Search -- Systems and Projects -- Digital Repository of Mathematical Formulae -- NNexus Reloaded -- E-books and Graphics with LATExml -- System Description: MathHub.info -- Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description -- System Description: A Semantics-Aware LATEX-to-Office Converter -- Math Indexer and Searcher Web Interface: Towards Fulfillment of Mathematicians? Information Needs -- SAT-Enhanced Mizar Proof Checking -- A Framework for Formal Reasoning about Geometrical Optics. 330 $aThis book constitutes the joint refereed proceedings of Calculemus 2014, Digital Mathematics Libraries, DML 2014, Mathematical Knowledge Management, MKM 2014, and Systems and Projects, S&P 2014, held in Coimbra, Portugal, during July 7-11, 2014 as four tracks of CICM 2014, the Conferences on Intelligent Computer Mathematics. The 26 full papers and 9 Systems and Projects descriptions presented together with 5 invited talks were carefully reviewed and selected from a total of 55 submissions. The Calculemus track of CICM examines the integration of symbolic computation and mechanized reasoning. The Digital Mathematics Libraries track - evolved from the DML workshop series - features math-aware technologies, standards, algorithms and processes towards the fulfillment of the dream of a global DML. The Mathematical Knowledge Management track of CICM is concerned with all aspects of managing mathematical knowledge in the informal, semi-formal, and formal settings. The Systems and Projects track presents short descriptions of existing systems or on-going projects in the areas of all the other tracks of the conference. 410 0$aLecture Notes in Artificial Intelligence ;$v8543 606 $aComputer science?Mathematics 606 $aArtificial intelligence 606 $aMathematical logic 606 $aNatural language processing (Computer science) 606 $aInformation storage and retrieval 606 $aSymbolic and Algebraic Manipulation$3https://scigraph.springernature.com/ontologies/product-market-codes/I17052 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 606 $aMath Applications in Computer Science$3https://scigraph.springernature.com/ontologies/product-market-codes/I17044 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 606 $aNatural Language Processing (NLP)$3https://scigraph.springernature.com/ontologies/product-market-codes/I21040 606 $aInformation Storage and Retrieval$3https://scigraph.springernature.com/ontologies/product-market-codes/I18032 615 0$aComputer science?Mathematics. 615 0$aArtificial intelligence. 615 0$aMathematical logic. 615 0$aNatural language processing (Computer science). 615 0$aInformation storage and retrieval. 615 14$aSymbolic and Algebraic Manipulation. 615 24$aArtificial Intelligence. 615 24$aMath Applications in Computer Science. 615 24$aMathematical Logic and Formal Languages. 615 24$aNatural Language Processing (NLP). 615 24$aInformation Storage and Retrieval. 676 $a512 702 $aWatt$b Stephen M$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aSexton$b Alan$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aDavenport$b James H$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aSojka$b Petr$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aUrban$b Josef$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910484944603321 996 $aIntelligent Computer Mathematics$93552027 997 $aUNINA