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

Πίνακας περιεχομένων:

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