Borrow it
Coverart for item
The Resource 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.)

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

Creator
Editor
Contributor
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
Language
eng
Work
Publication
Extent
1 online resource (xx, 458 pages)
Note
  • International conference proceedings
  • Includes author index
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
Isbn
9783319084343
Instance
Label
Intelligent computer mathematics : International Conference, CICM 2014, Coimbra, Portugal, July 7-11, 2014 : proceedings
Title
Intelligent computer mathematics
Title remainder
International Conference, CICM 2014, Coimbra, Portugal, July 7-11, 2014 : proceedings
Statement of responsibility
Stephen M. Watt, James H. Davenport, Alan P. Sexton, Petr Sojka, Josef Urban (Eds.)
Title variation
CICM 2014
Creator
Contributor
Editor
Subject
Genre
Language
eng
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
Member of
Cataloging source
NLGGC
Dewey number
004.01/51
Illustrations
illustrations
Index
index present
LC call number
QA76.9.M35
Literary form
non fiction
http://bibfra.me/vocab/lite/meetingDate
2014
http://bibfra.me/vocab/lite/meetingName
CICM (Conference)
Nature of contents
dictionaries
http://library.link/vocab/relatedWorkOrContributorName
  • Watt, Stephen M.
  • Davenport, James H.
  • Sexton, Alan P.
  • Sojka, Petr
  • Urban, Josef
Series statement
  • Lecture notes in artificial intelligence
  • LNCS sublibrary. SL 7, Artificial intelligence
Series volume
8543
http://library.link/vocab/subjectName
  • Computer science
  • Artificial intelligence
  • Artificial intelligence
  • Computer science
Label
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.)
Instantiates
Publication
Copyright
Note
  • International conference proceedings
  • Includes author index
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
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
Control code
882411174
Extent
1 online resource (xx, 458 pages)
Form of item
online
Isbn
9783319084343
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Other control number
10.1007/978-3-319-08434-3
Other physical details
illustrations
Specific material designation
remote
System control number
(OCoLC)882411174
Label
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.)
Publication
Copyright
Note
  • International conference proceedings
  • Includes author index
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
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
Control code
882411174
Extent
1 online resource (xx, 458 pages)
Form of item
online
Isbn
9783319084343
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Other control number
10.1007/978-3-319-08434-3
Other physical details
illustrations
Specific material designation
remote
System control number
(OCoLC)882411174

Subject

Genre

Member of

Library Locations

    • Thomas Jefferson LibraryBorrow it
      1 University Blvd, St. Louis, MO, 63121, US
      38.710138 -90.311107

Library Links

Structured data from the Bibframe namespace is licensed under the Creative Commons Attribution 4.0 International License by University of Missouri-St. Louis Libraries. Additional terms may apply to data associated with third party namespaces.
Processing Feedback ...