000 05907nam a22006255i 4500
001 978-3-540-31431-8
003 DE-He213
005 20240730193401.0
007 cr nn 008mamaa
008 100419s2006 gw | s |||| 0|eng d
020 _a9783540314318
_9978-3-540-31431-8
024 7 _a10.1007/11618027
_2doi
050 4 _aQ334-342
050 4 _aTA347.A78
072 7 _aUYQ
_2bicssc
072 7 _aCOM004000
_2bisacsh
072 7 _aUYQ
_2thema
082 0 4 _a006.3
_223
245 1 0 _aMathematical Knowledge Management
_h[electronic resource] :
_b4th International Conference, MKM 2005, Bremen, Germany, July 15-17, 2005, Revised Selected Papers /
_cedited by Michael Kohlhase.
250 _a1st ed. 2006.
264 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg :
_bImprint: Springer,
_c2006.
300 _aXII, 408 p.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aLecture Notes in Artificial Intelligence,
_x2945-9141 ;
_v3863
505 0 _aSession I: Foundations -- A Proof-Theoretic Approach to Hierarchical Math Library Organization -- An Exploration in the Space of Mathematical Knowledge -- Session II: Authoring -- Authoring Presentation for openmath -- Translating Mathematical Vernacular into Knowledge Repositories -- Assisted Proof Document Authoring -- Session III: Representations -- A Tough Nut for Mathematical Knowledge Management -- Textbook Proofs Meet Formal Logic - The Problem of Underspecification and Granularity -- Processing Textbook-Style Matrices -- Session IV: Proving -- A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity -- Impasse-Driven Reasoning in Proof Planning -- Literate Proving: Presenting and Documenting Formal Proofs -- Session V: MKManagement Tools -- Semantic Matching for Mathematical Services -- Mathematical Knowledge Browser with Automatic Hyperlink Detection -- A Database of Glyphs for OCR of Mathematical Documents -- Session VI: Documents -- Toward an Object-Oriented Structure for Mathematical Text -- Explanation in Natural Language of ?????-Terms -- Engineering Mathematical Knowledge -- Session VII: MKM Case Studies -- Computational Origami of a Morley's Triangle -- Designing Diagrammatic Catalogues of Types of Basic Interval Equation: A Case Study -- Gröbner Bases - Theory Refinement in the Mizar System -- Session VIII: Course Materials -- An Interactive Algebra Course with Formalised Proofs and Definitions -- Interactive Learning and Mathematical Calculus -- Session IX: Migration -- XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy -- Determining Empirical Characteristics of Mathematical Expression Use -- Transformations of MML Database's Elements -- Translating a Fragment of Weak Type Theory into Type Theory with Open Terms.
520 _aThis volume contains the proceedings of the Fourth International Conference on Mathematical Knowledge Management MKM 2005 held July 15-17, 2005 at - ternational University Bremen, Germany. Previous conferences have been at the Research Institute for Symbolic Computation (RISC) Linz, Austria (September 2001), at Bertinoro, Italy (March 2003), and Bialowiecze, Poland (September 2004). Mathematical knowledge management (MKM) is a ?eld in the intersection of mathematics and computer science, providing new techniques for managing the enormous volume of mathematical knowledge available in current mathematical sources and making it available through the new developments in information technology. The annual MKM Conference brings together mathematicians, software - velopers, publishing companies, math organizations, math users, and educators to exchange their views and approaches, current activities and new initiatives. For the ?rst time, MKM 2005 chose to have post-conference proceedings, as otherwise the submission deadline would have collided with other conferences and crimped time since MKM 2004 in September 2004. The decision also faci- tatedkeepingtheconferenceopentonewideasaswellaskeepingupthematurity of the papers necessary for inclusion into archival proceedings. With a May 15 deadline, MKM 2005 received 38 submissions. Each submission was reviewed by at least three programme committee members. The committee decided to - cept 27 papers for presentation at the conference. Out of these, 26 papers were accepted for publication in the conference proceedings after re-evaluation by the Programme Committee since they included signi?cant improvements triggered by the referee reports and the discussions at the conference.
650 0 _aArtificial intelligence.
_93407
650 0 _aComputer networks .
_931572
650 0 _aDatabase management.
_93157
650 0 _aInformation storage and retrieval systems.
_922213
650 0 _aApplication software.
_9153457
650 0 _aMathematics.
_911584
650 1 4 _aArtificial Intelligence.
_93407
650 2 4 _aComputer Communication Networks.
_9153458
650 2 4 _aDatabase Management.
_93157
650 2 4 _aInformation Storage and Retrieval.
_923927
650 2 4 _aComputer and Information Systems Applications.
_9153459
650 2 4 _aMathematics.
_911584
700 1 _aKohlhase, Michael.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9153460
710 2 _aSpringerLink (Online service)
_9153461
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783540314301
776 0 8 _iPrinted edition:
_z9783540819899
830 0 _aLecture Notes in Artificial Intelligence,
_x2945-9141 ;
_v3863
_9153462
856 4 0 _uhttps://doi.org/10.1007/11618027
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
942 _cELN
999 _c94727
_d94727