LEADER 07397nam 22008055 450 001 996199993903316 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$b[electronic resource] $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 $a996199993903316 996 $aIntelligent Computer Mathematics$92149623 997 $aUNISA LEADER 02388nas 2200697-a 450 001 996210640803316 005 20230227213019.0 035 $a(OCoLC)42415888 035 $a(CKB)954921381805 035 $a(CONSER)--2013250659 035 $a(MiAaPQ)36341 035 $a(EXLCZ)99954921381805 100 $a19990922a19829999 s-- - 101 0 $aeng 135 $aurunu|||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aInternational financial law review 210 $aLondon $cEuromoney Publications 300 $aRefereed/Peer-reviewed 311 $a0262-6969 517 1 $aIFLR magazine 517 1 $aIFLR 531 $aINTERNATIONAL FINANCIAL LAW REVIE 606 $aFinance$xLaw and legislation$vPeriodicals 606 $aCommercial law$vPeriodicals 606 $aContracts$vPeriodicals 606 $aInternational business enterprises$xLaw and legislation$vPeriodicals 606 $aFinances$xDroit$vPériodiques 606 $aDroit commercial$vPériodiques 606 $aContrats$vPériodiques 606 $aEntreprises multinationales$xDroit$vPériodiques 606 $aCommercial law$2fast$3(OCoLC)fst00869502 606 $aContracts$2fast$3(OCoLC)fst00876969 606 $aFinance$xLaw and legislation$2fast$3(OCoLC)fst00924391 606 $aInternational business enterprises$xLaw and legislation$2fast$3(OCoLC)fst00976808 606 $aInternationaal handelsrecht$2gtt 606 $aFinanciële aspecten$2gtt 606 $aInternationaal bedrijfsleven$2gtt 608 $aPeriodicals.$2fast 608 $aPeriodicals.$2lcgft 615 0$aFinance$xLaw and legislation 615 0$aCommercial law 615 0$aContracts 615 0$aInternational business enterprises$xLaw and legislation 615 6$aFinances$xDroit 615 6$aDroit commercial 615 6$aContrats 615 6$aEntreprises multinationales$xDroit 615 7$aCommercial law. 615 7$aContracts. 615 7$aFinance$xLaw and legislation. 615 7$aInternational business enterprises$xLaw and legislation. 615 17$aInternationaal handelsrecht. 615 17$aFinanciële aspecten. 615 17$aInternationaal bedrijfsleven. 906 $aNEWSPAPER 912 $a996210640803316 996 $aInternational financial law review$91412468 997 $aUNISA