Intelligent Computer Mathematics International Conference, CICM 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Watt, Stephen M. (Επιμελητής έκδοσης), Davenport, James H. (Επιμελητής έκδοσης), Sexton, Alan P. (Επιμελητής έκδοσης), Sojka, Petr (Επιμελητής έκδοσης), Urban, Josef (Επιμελητής έκδοσης)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Cham : Springer International Publishing : Imprint: Springer, 2014.
• Σειρά: Lecture Notes in Computer Science, 8543
• Θέματα: Computer science.; Mathematical logic.; Computer science > Mathematics.; Information storage and retrieval.; Artificial intelligence.; Text processing (Computer science).; Computer Science.; Symbolic and Algebraic Manipulation.; Artificial Intelligence (incl. Robotics).; Math Applications in Computer Science.; Mathematical Logic and Formal Languages.; Document Preparation and Text Processing.; Information Storage and Retrieval.

 This 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. 

 Invited 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.