Intelligent computer mathematics : International Conference, CICM 2014, Coimbra, Portugal, July 7-11, 2014 : proceedings / Stephen M. Watt, James H. Davenport, Alan P. Sexton, Petr Sojka, Josef Urban (Eds.).

By: CICM (Conference) (2014 : Coimbra, Portugal)
Contributor(s): Watt, Stephen M [editor.] | Davenport, James H [editor.] | Sexton, Alan P [editor.] | Sojka, Petr [editor.] | Urban, Josef [editor.]
Material type: TextTextSeries: SerienbezeichnungLecture notes in computer science: 8543.; Lecture notes in computer science: ; LNCS sublibrary: Publisher: Cham : Springer, [2014]Copyright date: ©2014Description: 1 online resource (xx, 458 pages) : illustrationsContent type: text Media type: computer Carrier type: online resourceISBN: 9783319084343; 3319084348Other title: CICM 2014Subject(s): Computer science -- Mathematics -- Congresses | Artificial intelligence -- Mathematics -- Congresses | Artificial intelligence -- Mathematics | Computer science -- Mathematics | computerwetenschappen | computer sciences | wiskunde | mathematics | informatieontsluiting | information retrieval | informatieopslag | information storage | publiceren | publishing | algebra | kunstmatige intelligentie | artificial intelligence | logica | logic | Information and Communication Technology (General) | Informatie- en communicatietechnologie (algemeen)Genre/Form: Electronic books. | Conference papers and proceedings. Additional physical formats: Printed edition:: No titleDDC classification: 004.01/51 LOC classification: QA76.9.M35Online resources: Click here to access online
Contents:
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.
Summary: 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.
Tags from this library: No tags from this library for this title. Log in to add tags.
    Average rating: 0.0 (0 votes)
Item type Current location Collection Call number Status Date due Barcode Item holds
eBook eBook e-Library

Electronic Book@IST

EBook Available
Total holds: 0

International conference proceedings.

Includes author index.

Online resource; title from PDF title page (SpringerLink, viewed July 9, 2014).

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.

There are no comments for this item.

to post a comment.

Powered by Koha