MARC details
| 000 -LEADER |
|---|
| fixed length control field |
06139cam a2200781 a 4500 |
| 001 - CONTROL NUMBER |
|---|
| control field |
ocn654396289 |
| 003 - CONTROL NUMBER IDENTIFIER |
|---|
| control field |
OCoLC |
| 005 - DATE AND TIME OF LATEST TRANSACTION |
|---|
| control field |
20250703155828.0 |
| 006 - FIXED-LENGTH DATA ELEMENTS--ADDITIONAL MATERIAL CHARACTERISTICS |
|---|
| fixed length control field |
m o d |
| 007 - PHYSICAL DESCRIPTION FIXED FIELD--GENERAL INFORMATION |
|---|
| fixed length control field |
cr cn||||||||| |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION |
|---|
| fixed length control field |
100810s2010 gw a ob 101 0 eng d |
| 040 ## - CATALOGING SOURCE |
|---|
| Original cataloging agency |
GW5XE |
| Language of cataloging |
eng |
| Description conventions |
pn |
| Transcribing agency |
GW5XE |
| Modifying agency |
GZM |
| -- |
CEF |
| -- |
E7B |
| -- |
OCLCQ |
| -- |
OCLCO |
| -- |
OCLCA |
| -- |
OCLCQ |
| -- |
OCLCA |
| -- |
OCLCF |
| -- |
BEDGE |
| -- |
OCLCA |
| -- |
OCLCO |
| -- |
OCL |
| -- |
OCLCO |
| -- |
OCLCQ |
| -- |
IOG |
| -- |
BUF |
| -- |
OCLCA |
| -- |
OCLCQ |
| -- |
LQU |
| -- |
COM |
| -- |
OCLCO |
| -- |
OCLCQ |
| -- |
OCLCL |
| 019 ## - |
|---|
| -- |
769770480 |
| -- |
1137251025 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
9783642141287 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
3642141285 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| Canceled/invalid ISBN |
9783642141270 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| Canceled/invalid ISBN |
3642141277 |
| 024 8# - OTHER STANDARD IDENTIFIER |
|---|
| Standard number or code |
10.1007/978-3-642-14 |
| 029 1# - (OCLC) |
|---|
| OCLC library identifier |
AU@ |
| System control number |
000048714750 |
| 029 1# - (OCLC) |
|---|
| OCLC library identifier |
NZ1 |
| System control number |
13517743 |
| 035 ## - SYSTEM CONTROL NUMBER |
|---|
| System control number |
(OCoLC)654396289 |
| Canceled/invalid control number |
(OCoLC)769770480 |
| -- |
(OCoLC)1137251025 |
| 037 ## - SOURCE OF ACQUISITION |
|---|
| Stock number |
978-3-642-14127-0 |
| Source of stock number/acquisition |
Springer |
| Note |
http://www.springerlink.com |
| 050 #4 - LIBRARY OF CONGRESS CALL NUMBER |
|---|
| Classification number |
QA155.7.E4 |
| Item number |
C35 2010 |
| 082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER |
|---|
| Classification number |
512.0285 |
| Edition number |
22 |
| 049 ## - LOCAL HOLDINGS (OCLC) |
|---|
| Holding library |
MAIN |
| 111 2# - MAIN ENTRY--MEETING NAME |
|---|
| Meeting name or jurisdiction name as entry element |
AISC (Conference) |
| Number of part/section/meeting |
(10th : |
| Date of meeting |
2010 : |
| Location of meeting |
Paris, France) |
| 9 (RLIN) |
39038 |
| 245 10 - TITLE STATEMENT |
|---|
| Title |
Intelligent computer mathematics : |
| Remainder of title |
10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010, Paris, France, July 5-10, 2010 : proceedings / |
| Statement of responsibility, etc. |
Serge Autexier [and others] (eds.). |
| 246 30 - VARYING FORM OF TITLE |
|---|
| Title proper/short title |
AISC 2010 |
| 246 30 - VARYING FORM OF TITLE |
|---|
| Title proper/short title |
Calculemus 2010 |
| 246 30 - VARYING FORM OF TITLE |
|---|
| Title proper/short title |
MKM 2010 |
| 260 ## - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT) |
|---|
| Place of publication, distribution, etc. |
Berlin ; |
| -- |
New York : |
| Name of publisher, distributor, etc. |
Springer, |
| Date of publication, distribution, etc. |
©2010. |
| 300 ## - PHYSICAL DESCRIPTION |
|---|
| Extent |
1 online resource (xv, 469 pages) : |
| Other physical details |
illustrations |
| 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 |
| 490 1# - SERIES STATEMENT |
|---|
| Series statement |
Lecture notes in computer science, |
| International Standard Serial Number |
0302-9743 ; |
| Volume/sequential designation |
6167. |
| Series statement |
Lecture notes in artificial intelligence |
| 490 1# - SERIES STATEMENT |
|---|
| Series statement |
LNCS sublibrary. SL 7, Artificial intelligence |
| 504 ## - BIBLIOGRAPHY, ETC. NOTE |
|---|
| Bibliography, etc |
Includes bibliographical references and index. |
| 505 0# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
Contributions to AISC 2010 -- The Challenges of Multivalued "Functions" -- The Dynamic Dictionary of Mathematical Functions -- A Revisited Perspective on Symbolic Mathematical Computing and Artificial Intelligence -- I-Terms in Ordered Resolution and Superposition Calculi: Retrieving Lost Completeness -- Structured Formal Development with Quotient Types in Isabelle/HOL -- Instantiation of SMT Problems Modulo Integers -- On Krawtchouk Transforms -- A Mathematical Model of the Competition between Acquired Immunity and Virus -- Some Notes upon "When Does $]]> Equal Sat?" -- How to Correctly Prune Tropical Trees -- From Matrix Interpretations over the Rationals to Matrix Interpretations over the Naturals -- Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar -- Contributions to Calculemus 2010 -- Some Considerations on the Usability of Interactive Provers -- Mechanized Mathematics -- Formal Proof of SCHUR Conjugate Function -- Symbolic Domain Decomposition -- A Formal Quantifier Elimination for Algebraically Closed Fields -- Computing in Coq with Infinite Algebraic Data Structures -- Formally Verified Conditions for Regularity of Interval Matrices -- Reducing Expression Size Using Rule-Based Integration -- A Unified Formal Description of Arithmetic and Set Theoretical Data Types -- Contributions to MKM 2010 -- Against Rigor -- Smart Matching -- Electronic Geometry Textbook: A Geometric Textbook Knowledge Management System -- An OpenMath Content Dictionary for Tensor Concepts -- On Duplication in Mathematical Repositories -- Adapting Mathematical Domain Reasoners -- Integrating Multiple Sources to Answer Questions in Algebraic Topology -- An Integrated Development Environment for Collections -- Proofs, Proofs, Proofs, and Proofs -- Dimensions of Formality: A Case Study for MKM in Software Engineering -- Towards MKM in the Large: Modular Representation and Scalable Software Architecture -- The Formulator MathML Editor Project: User-F riendly Authoring of Content Markup Documents -- Notations Around the World: Census and Exploitation -- Evidence Algorithm and System for Automated Deduction: A Retrospective View -- On Building a Knowledge Base for Stability Theory -- Proviola: A Tool for Proof Re-animation -- A Wiki for Mizar: Motivation, Considerations, and Initial Prototype. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Algebra |
| General subdivision |
Data processing |
| Form subdivision |
Congresses. |
| 9 (RLIN) |
14649 |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Mathematical analysis |
| General subdivision |
Data processing |
| Form subdivision |
Congresses. |
| 9 (RLIN) |
22096 |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Logic, Symbolic and mathematical |
| Form subdivision |
Congresses. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Knowledge management |
| Form subdivision |
Congresses. |
| 9 (RLIN) |
16482 |
| 650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Algèbre |
| General subdivision |
Informatique |
| Form subdivision |
Congrès. |
| 9 (RLIN) |
25053 |
| 650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Analyse mathématique |
| General subdivision |
Informatique |
| Form subdivision |
Congrès. |
| 9 (RLIN) |
966964 |
| 650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Logique symbolique et mathématique |
| Form subdivision |
Congrès. |
| 650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Gestion des connaissances |
| Form subdivision |
Congrès. |
| 9 (RLIN) |
19247 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Informatique. |
| Source of heading or term |
eclas |
| 9 (RLIN) |
14930 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Algebra |
| General subdivision |
Data processing. |
| Source of heading or term |
fast |
| Authority record control number |
(OCoLC)fst00804890 |
| 9 (RLIN) |
14650 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Knowledge management. |
| Source of heading or term |
fast |
| Authority record control number |
(OCoLC)fst00988184 |
| 9 (RLIN) |
1209 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Logic, Symbolic and mathematical. |
| Source of heading or term |
fast |
| Authority record control number |
(OCoLC)fst01002068 |
| 9 (RLIN) |
1341 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Mathematical analysis |
| General subdivision |
Data processing. |
| Source of heading or term |
fast |
| Authority record control number |
(OCoLC)fst01012070 |
| 9 (RLIN) |
22098 |
| 655 #2 - INDEX TERM--GENRE/FORM |
|---|
| Genre/form data or focus term |
Congress |
| 9 (RLIN) |
11670 |
| 655 #7 - INDEX TERM--GENRE/FORM |
|---|
| Genre/form data or focus term |
Conference papers and proceedings. |
| Source of term |
fast |
| Authority record control number |
(OCoLC)fst01423772 |
| 9 (RLIN) |
6065 |
| 655 #7 - INDEX TERM--GENRE/FORM |
|---|
| Genre/form data or focus term |
Conference papers and proceedings. |
| Source of term |
lcgft |
| 9 (RLIN) |
6065 |
| 655 #7 - INDEX TERM--GENRE/FORM |
|---|
| Genre/form data or focus term |
Actes de congrès. |
| Source of term |
rvmgf |
| 9 (RLIN) |
609890 |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Autexier, Serge. |
| 9 (RLIN) |
31138 |
| 711 2# - ADDED ENTRY--MEETING NAME |
|---|
| Meeting name or jurisdiction name as entry element |
Calculemus 2010 |
| Date of meeting |
(2010 : |
| Location of meeting |
Paris, France) |
| 9 (RLIN) |
39040 |
| 711 2# - ADDED ENTRY--MEETING NAME |
|---|
| Meeting name or jurisdiction name as entry element |
MKM (Conference) |
| Number of part/section/meeting |
(9th : |
| Date of meeting |
2010 : |
| Location of meeting |
Paris, France) |
| 9 (RLIN) |
39041 |
| 758 ## - |
|---|
| -- |
has work: |
| -- |
Intelligent computer mathematics (Text) |
| -- |
https://id.oclc.org/worldcat/entity/E39PCGgPkyfKwVVqhHqtWJyMHd |
| -- |
https://id.oclc.org/worldcat/ontology/hasWork |
| 776 08 - ADDITIONAL PHYSICAL FORM ENTRY |
|---|
| Relationship information |
Print version: |
| Title |
Intelligent Computer Mathematics. |
| Place, publisher, and date of publication |
Springer-Verlag New York Inc 2010 |
| International Standard Book Number |
9783642141270 |
| Record control number |
(DLC) 2010929251 |
| -- |
(OCoLC)646114563 |
| 830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE |
|---|
| Uniform title |
Lecture notes in computer science ; |
| Volume number/sequential designation |
6167. |
| 830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE |
|---|
| Uniform title |
Lecture notes in computer science. |
| Name of part/section of a work |
Lecture notes in artificial intelligence. |
| 9 (RLIN) |
14916 |
| 830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE |
|---|
| Uniform title |
LNCS sublibrary. |
| Number of part/section of a work |
SL 7, |
| Name of part/section of a work |
Artificial intelligence. |
| 9 (RLIN) |
20712 |
| 856 40 - ELECTRONIC LOCATION AND ACCESS |
|---|
| Uniform Resource Identifier |
<a href="https://link.springer.com/10.1007/978-3-642-14128-7">https://link.springer.com/10.1007/978-3-642-14128-7</a> |
| 938 ## - |
|---|
| -- |
ebrary |
| -- |
EBRY |
| -- |
ebr10399978 |
| 994 ## - |
|---|
| -- |
92 |
| -- |
ATIST |