Intelligent Computer Mathematics (Record no. 208974)
[ view plain ]
| 000 -LEADER | |
|---|---|
| fixed length control field | 06133nam a22006135i 4500 |
| 001 - CONTROL NUMBER | |
| control field | 978-3-319-08434-3 |
| 003 - CONTROL NUMBER IDENTIFIER | |
| control field | DE-He213 |
| 005 - DATE AND TIME OF LATEST TRANSACTION | |
| control field | 20160302172923.0 |
| 007 - PHYSICAL DESCRIPTION FIXED FIELD--GENERAL INFORMATION | |
| fixed length control field | cr nn 008mamaa |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION | |
| fixed length control field | 140630s2014 gw | s |||| 0|eng d |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| International Standard Book Number | 9783319084343 |
| -- | 978-3-319-08434-3 |
| 024 7# - OTHER STANDARD IDENTIFIER | |
| Standard number or code | 10.1007/978-3-319-08434-3 |
| Source of number or code | doi |
| 050 #4 - LIBRARY OF CONGRESS CALL NUMBER | |
| Classification number | QA76.9.M35 |
| 072 #7 - SUBJECT CATEGORY CODE | |
| Subject category code | UYAM |
| Source | bicssc |
| 072 #7 - SUBJECT CATEGORY CODE | |
| Subject category code | COM018000 |
| Source | bisacsh |
| 072 #7 - SUBJECT CATEGORY CODE | |
| Subject category code | MAT002000 |
| Source | bisacsh |
| 082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER | |
| Classification number | 005.131 |
| Edition number | 23 |
| 245 10 - TITLE STATEMENT | |
| Title | Intelligent Computer Mathematics |
| Medium | [electronic resource] : |
| Remainder of title | International Conference, CICM 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings / |
| Statement of responsibility, etc. | edited by Stephen M. Watt, James H. Davenport, Alan P. Sexton, Petr Sojka, Josef Urban. |
| 264 #1 - PRODUCTION, PUBLICATION, DISTRIBUTION, MANUFACTURE, AND COPYRIGHT NOTICE | |
| Place of production, publication, distribution, manufacture | Cham : |
| Name of producer, publisher, distributor, manufacturer | Springer International Publishing : |
| -- | Imprint: Springer, |
| Date of production, publication, distribution, manufacture, or copyright notice | 2014. |
| 300 ## - PHYSICAL DESCRIPTION | |
| Extent | XX, 458 p. 111 illus. |
| Other physical details | online resource. |
| 336 ## - CONTENT TYPE | |
| Content type term | text |
| Content type code | txt |
| Source | rdacontent |
| 337 ## - MEDIA TYPE | |
| Media type term | computer |
| Media type code | c |
| Source | rdamedia |
| 338 ## - CARRIER TYPE | |
| Carrier type term | online resource |
| Carrier type code | cr |
| Source | rdacarrier |
| 347 ## - DIGITAL FILE CHARACTERISTICS | |
| File type | text file |
| Encoding format | |
| Source | rda |
| 490 1# - SERIES STATEMENT | |
| Series statement | Lecture Notes in Computer Science, |
| International Standard Serial Number | 0302-9743 ; |
| Volume/sequential designation | 8543 |
| 505 0# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 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. |
| 520 ## - SUMMARY, ETC. | |
| Summary, etc. | 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. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Computer science. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Mathematical logic. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Computer science |
| General subdivision | Mathematics. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Information storage and retrieval. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Artificial intelligence. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Text processing (Computer science). |
| 650 14 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Computer Science. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Symbolic and Algebraic Manipulation. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Artificial Intelligence (incl. Robotics). |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Math Applications in Computer Science. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Mathematical Logic and Formal Languages. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Document Preparation and Text Processing. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Information Storage and Retrieval. |
| 700 1# - ADDED ENTRY--PERSONAL NAME | |
| Personal name | Watt, Stephen M. |
| Relator term | editor. |
| 700 1# - ADDED ENTRY--PERSONAL NAME | |
| Personal name | Davenport, James H. |
| Relator term | editor. |
| 700 1# - ADDED ENTRY--PERSONAL NAME | |
| Personal name | Sexton, Alan P. |
| Relator term | editor. |
| 700 1# - ADDED ENTRY--PERSONAL NAME | |
| Personal name | Sojka, Petr. |
| Relator term | editor. |
| 700 1# - ADDED ENTRY--PERSONAL NAME | |
| Personal name | Urban, Josef. |
| Relator term | editor. |
| 710 2# - ADDED ENTRY--CORPORATE NAME | |
| Corporate name or jurisdiction name as entry element | SpringerLink (Online service) |
| 773 0# - HOST ITEM ENTRY | |
| Title | Springer eBooks |
| 776 08 - ADDITIONAL PHYSICAL FORM ENTRY | |
| Relationship information | Printed edition: |
| International Standard Book Number | 9783319084336 |
| 830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE | |
| Uniform title | Lecture Notes in Computer Science, |
| International Standard Serial Number | 0302-9743 ; |
| Volume number/sequential designation | 8543 |
| 856 40 - ELECTRONIC LOCATION AND ACCESS | |
| Uniform Resource Identifier | <a href="http://dx.doi.org/10.1007/978-3-319-08434-3">http://dx.doi.org/10.1007/978-3-319-08434-3</a> |
| 912 ## - | |
| -- | ZDB-2-SCS |
| 912 ## - | |
| -- | ZDB-2-LNC |
No items available.