MARC details
| 000 -LEADER |
|---|
| fixed length control field |
06097nam a22006015i 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 |
20170628034205.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 |
| 100 1# - MAIN ENTRY--PERSONAL NAME |
|---|
| Personal name |
Watt, Stephen M. |
| Relator term |
editor. |
| 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 - |
|---|
| -- |
Cham : |
| -- |
Springer International Publishing : |
| -- |
Imprint: Springer, |
| -- |
2014. |
| 300 ## - PHYSICAL DESCRIPTION |
|---|
| Extent |
XX, 458 p. 111 illus. |
| Other physical details |
online resource. |
| 336 ## - |
|---|
| -- |
text |
| -- |
txt |
| -- |
rdacontent |
| 337 ## - |
|---|
| -- |
computer |
| -- |
c |
| -- |
rdamedia |
| 338 ## - |
|---|
| -- |
online resource |
| -- |
cr |
| -- |
rdacarrier |
| 347 ## - |
|---|
| -- |
text file |
| -- |
PDF |
| -- |
rda |
| 490 1# - SERIES STATEMENT |
|---|
| Series statement |
Lecture Notes in Computer Science, |
| International Standard Serial Number |
0302-9743 ; |
| Volume number/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 |
Algebra |
| General subdivision |
Data processing. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Information storage and retrieval systems. |
| 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 |
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 |
|---|
| Display text |
Printed edition: |
| International Standard Book Number |
9783319084336 |
| 830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE |
|---|
| Uniform title |
Lecture Notes in Computer Science, |
| -- |
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 |
