Towards Mechanized Mathematical Assistants (Record no. 85616)

000 -LEADER
fixed length control field 06278nam a22006495i 4500
001 - CONTROL NUMBER
control field 978-3-540-73086-6
003 - CONTROL NUMBER IDENTIFIER
control field DE-He213
005 - DATE AND TIME OF LATEST TRANSACTION
control field 20240730164346.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 100301s2007 gw | s |||| 0|eng d
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number 9783540730866
-- 978-3-540-73086-6
024 7# - OTHER STANDARD IDENTIFIER
Standard number or code 10.1007/978-3-540-73086-6
Source of number or code doi
050 #4 - LIBRARY OF CONGRESS CALL NUMBER
Classification number QA150-272
072 #7 - SUBJECT CATEGORY CODE
Subject category code PBF
Source bicssc
072 #7 - SUBJECT CATEGORY CODE
Subject category code MAT002000
Source bisacsh
072 #7 - SUBJECT CATEGORY CODE
Subject category code PBF
Source thema
082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER
Classification number 512
Edition number 23
245 10 - TITLE STATEMENT
Title Towards Mechanized Mathematical Assistants
Medium [electronic resource] :
Remainder of title 14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, Hagenberg, Austria, June 27-30, 2007, Proceedings /
Statement of responsibility, etc. edited by Manuel Kauers, Manfred Kerber, Robert Miner, Wolfgang Windsteiger.
250 ## - EDITION STATEMENT
Edition statement 1st ed. 2007.
264 #1 - PRODUCTION, PUBLICATION, DISTRIBUTION, MANUFACTURE, AND COPYRIGHT NOTICE
Place of production, publication, distribution, manufacture Berlin, Heidelberg :
Name of producer, publisher, distributor, manufacturer Springer Berlin Heidelberg :
-- Imprint: Springer,
Date of production, publication, distribution, manufacture, or copyright notice 2007.
300 ## - PHYSICAL DESCRIPTION
Extent XIII, 410 p.
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 PDF
Source rda
490 1# - SERIES STATEMENT
Series statement Lecture Notes in Artificial Intelligence,
International Standard Serial Number 2945-9141 ;
Volume/sequential designation 4573
505 0# - FORMATTED CONTENTS NOTE
Formatted contents note Contributions to Calculemus 2007 -- Executing in Common Lisp, Proving in ACL2 -- A Rational Reconstruction of a System for Experimental Mathematics -- Context Aware Calculation and Deduction -- Towards Constructive Homological Algebra in Type Theory -- What Might "Understand a Function" Mean? -- Biform Theories in Chiron -- Automatic Synthesis of Decision Procedures: A Case Study of Ground and Linear Arithmetic -- Certified Computer Algebra on Top of an Interactive Theorem Prover -- Quantifier Elimination for Approximate Factorization of Linear Partial Differential Operators -- Rule-Based Simplification in Vector-Product Spaces -- Contributions to MKM 2007 -- Mathematics and Scientific Markup -- The On-Line Encyclopedia of Integer Sequences -- First Steps on Using OpenMath to Add Proving Capabilities to Standard Dynamic Geometry Systems -- Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case -- A Framework for Interactive Proof -- Supporting User-Defined Notations When Integrating Scientific Text-Editors with Proof Assistance Systems -- Mizar Course in Logic and Set Theory -- Using Formal Concept Analysis in Mathematical Discovery -- Cooperative Repositories for Formal Proofs -- Revisions as an Essential Tool to Maintain Mathematical Repositories -- The Layers of Logiweb -- Formal Representation of Mathematics in a Dependently Typed Set Theory -- Restoring Natural Language as a Computerised Mathematics Input Method -- Narrative Structure of Mathematical Texts -- Reexamining the MKM Value Proposition: From Math Web Search to Math Web ReSearch -- Alternative Aggregates in Mizar -- An Approach to Mathematical Search Through Query Formulation and Data Normalization -- Extended Formula Normalization for ?-Retrieval and Sharing of Mathematical Knowledge.-Towards Mathematical Knowledge Management for Electrical Engineering -- Spurious Disambiguation Error Detection -- Methods of Relevance Ranking and Hit-content Generation in Math Search.
520 ## - SUMMARY, ETC.
Summary, etc. This volume contains the collected contributions of two conferences, Calcu- mus2007andMKM2007.Calculemus2007wasthe14thinaseriesofconferences dedicated to the integration of computer algebra systems (CAS) and automated deduction systems (ADS). MKM 2007 was the sixth International Conference on Mathematical Knowledge Management, an emerging interdisciplinary ?eld of research in the intersection of mathematics, computer science, library s- ence, and scienti?c publishing. Both conferences aimed to provide mechanized mathematical assistants. Although the two conferences have separate communities and separate foci, there is a signi?cant overlap in the interests in building mechanized mathem- ical assistants. For this reason it was decided to collocate the two events in 2007 for the ?rst time, at RISC in Hagenberg, Austria. The number and quality of the submissions show that this was a good decision. While the proceedings are shared, the submission process was separate. The responsibility for acc- tance/rejection rests completely with the two separate Program Committees. By this collocation we made a contribution against the fragmentation of communities which work on di?erent aspects of di?erent independent branches, traditional branches (e.g., computer algebra and theorem proving), as well as newly emerging ones (on user interfaces, knowledge management, theory exp- ration, etc.). This will also facilitate the development of integrated mechanized mathematical assistants that will be routinely used by mathematicians, c- puter scientists, and engineers in their every-day business.
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Algebra.
9 (RLIN) 21222
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Artificial intelligence.
9 (RLIN) 3407
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Data mining.
9 (RLIN) 3907
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Application software.
9 (RLIN) 84087
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Database management.
9 (RLIN) 3157
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Computer networks .
9 (RLIN) 31572
650 14 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Algebra.
9 (RLIN) 21222
650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Artificial Intelligence.
9 (RLIN) 3407
650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Data Mining and Knowledge Discovery.
9 (RLIN) 84089
650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Computer and Information Systems Applications.
9 (RLIN) 84091
650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Database Management.
9 (RLIN) 3157
650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Computer Communication Networks.
9 (RLIN) 84093
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Kauers, Manuel.
Relator term editor.
Relationship edt
-- http://id.loc.gov/vocabulary/relators/edt
9 (RLIN) 84094
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Kerber, Manfred.
Relator term editor.
Relationship edt
-- http://id.loc.gov/vocabulary/relators/edt
9 (RLIN) 84096
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Miner, Robert.
Relator term editor.
Relationship edt
-- http://id.loc.gov/vocabulary/relators/edt
9 (RLIN) 84097
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Windsteiger, Wolfgang.
Relator term editor.
Relationship edt
-- http://id.loc.gov/vocabulary/relators/edt
9 (RLIN) 84099
710 2# - ADDED ENTRY--CORPORATE NAME
Corporate name or jurisdiction name as entry element SpringerLink (Online service)
9 (RLIN) 84101
773 0# - HOST ITEM ENTRY
Title Springer Nature eBook
776 08 - ADDITIONAL PHYSICAL FORM ENTRY
Relationship information Printed edition:
International Standard Book Number 9783540730835
776 08 - ADDITIONAL PHYSICAL FORM ENTRY
Relationship information Printed edition:
International Standard Book Number 9783540839576
830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE
Uniform title Lecture Notes in Artificial Intelligence,
International Standard Serial Number 2945-9141 ;
Volume/sequential designation 4573
9 (RLIN) 84103
856 40 - ELECTRONIC LOCATION AND ACCESS
Uniform Resource Identifier <a href="https://doi.org/10.1007/978-3-540-73086-6">https://doi.org/10.1007/978-3-540-73086-6</a>
912 ## -
-- ZDB-2-SCS
912 ## -
-- ZDB-2-SXCS
912 ## -
-- ZDB-2-LNC
942 ## - ADDED ENTRY ELEMENTS (KOHA)
Koha item type eBooks-Lecture Notes in CS

No items available.