000 06545nam a22006495i 4500
001 978-3-319-08434-3
003 DE-He213
005 20240423125217.0
007 cr nn 008mamaa
008 140630s2014 sz | 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 _aCOM014000
_2bisacsh
072 7 _aUYAM
_2thema
082 0 4 _a005.131
_223
245 1 0 _aIntelligent Computer Mathematics
_h[electronic resource] :
_bCICM 2014 Joint Events: Calculemus, DML, MKM, and Systems and Projects 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings /
_cedited by Stephen M. Watt, Alan Sexton, James H. Davenport, Petr Sojka, Josef Urban.
250 _a1st ed. 2014.
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 Artificial Intelligence,
_x2945-9141 ;
_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
_xMathematics.
650 0 _aArtificial intelligence.
650 0 _aMachine theory.
650 0 _aNatural language processing (Computer science).
650 0 _aInformation storage and retrieval systems.
650 1 4 _aSymbolic and Algebraic Manipulation.
650 2 4 _aArtificial Intelligence.
650 2 4 _aMathematical Applications in Computer Science.
650 2 4 _aFormal Languages and Automata Theory.
650 2 4 _aNatural Language Processing (NLP).
650 2 4 _aInformation Storage and Retrieval.
700 1 _aWatt, Stephen M.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
700 1 _aSexton, Alan.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
700 1 _aDavenport, James H.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
700 1 _aSojka, Petr.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
700 1 _aUrban, Josef.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
710 2 _aSpringerLink (Online service)
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783319084336
776 0 8 _iPrinted edition:
_z9783319084350
830 0 _aLecture Notes in Artificial Intelligence,
_x2945-9141 ;
_v8543
856 4 0 _uhttps://doi.org/10.1007/978-3-319-08434-3
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
942 _cSPRINGER
999 _c175450
_d175450