000 06149nam a22006255i 4500
001 978-3-319-08434-3
003 DE-He213
005 20200421112050.0
007 cr nn 008mamaa
008 140630s2014 gw | s |||| 0|eng d
020 _a9783319084343
_9978-3-319-08434-3
024 7 _a10.1007/978-3-319-08434-3
_2doi
050 4 _aQA76.9.M35
072 7 _aUYAM
_2bicssc
072 7 _aCOM018000
_2bisacsh
072 7 _aMAT002000
_2bisacsh
082 0 4 _a005.131
_223
245 1 0 _aIntelligent Computer Mathematics
_h[electronic resource] :
_bInternational Conference, CICM 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings /
_cedited by Stephen M. Watt, James H. Davenport, Alan P. Sexton, Petr Sojka, Josef Urban.
264 1 _aCham :
_bSpringer International Publishing :
_bImprint: Springer,
_c2014.
300 _aXX, 458 p. 111 illus.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aLecture Notes in Computer Science,
_x0302-9743 ;
_v8543
505 0 _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.
520 _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.
650 0 _aComputer science.
650 0 _aMathematical logic.
650 0 _aComputer science
_xMathematics.
650 0 _aInformation storage and retrieval.
650 0 _aArtificial intelligence.
650 0 _aText processing (Computer science).
650 1 4 _aComputer Science.
650 2 4 _aSymbolic and Algebraic Manipulation.
650 2 4 _aArtificial Intelligence (incl. Robotics).
650 2 4 _aMath Applications in Computer Science.
650 2 4 _aMathematical Logic and Formal Languages.
650 2 4 _aDocument Preparation and Text Processing.
650 2 4 _aInformation Storage and Retrieval.
700 1 _aWatt, Stephen M.
_eeditor.
700 1 _aDavenport, James H.
_eeditor.
700 1 _aSexton, Alan P.
_eeditor.
700 1 _aSojka, Petr.
_eeditor.
700 1 _aUrban, Josef.
_eeditor.
710 2 _aSpringerLink (Online service)
773 0 _tSpringer eBooks
776 0 8 _iPrinted edition:
_z9783319084336
830 0 _aLecture Notes in Computer Science,
_x0302-9743 ;
_v8543
856 4 0 _uhttp://dx.doi.org/10.1007/978-3-319-08434-3
912 _aZDB-2-SCS
912 _aZDB-2-LNC
942 _cEBK
999 _c57129
_d57129