LEADER 05496nam 22008655 450 001 9910143881103321 005 20251116234301.0 010 $a3-540-36469-2 024 7 $a10.1007/3-540-36469-2 035 $a(CKB)1000000000211928 035 $a(SSID)ssj0000324680 035 $a(PQKBManifestationID)11912691 035 $a(PQKBTitleCode)TC0000324680 035 $a(PQKBWorkID)10332240 035 $a(PQKB)11689312 035 $a(DE-He213)978-3-540-36469-6 035 $a(MiAaPQ)EBC3063715 035 $a(MiAaPQ)EBC6283589 035 $a(PPN)155197290 035 $a(BIP)13523238 035 $a(BIP)8159038 035 $a(EXLCZ)991000000000211928 100 $a20121227d2003 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aMathematical Knowledge Management $eSecond International Conference, MKM 2003 Bertinoro, Italy, February 16-18, 2003 /$fedited by Andrea Asperti, Bruno Buchberger, James Harold Davenport 205 $a1st ed. 2003. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2003. 215 $a1 online resource (X, 230 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v2594 300 $aBibliographic Level Mode of Issuance: Monograph 311 08$a3-540-00568-4 320 $aIncludes bibliographical references and index. 327 $aRegular Contributions -- Digitisation, Representation, and Formalisation Digital Libraries of Mathematics -- MKM from Book to Computer: A Case Study -- From Proof-Assistants to Distributed Libraries of Mathematics: Tips and Pitfalls -- Managing Digital Mathematical Discourse -- NAG Library Documentation -- On the Roles of LATEX and MathML in Encoding and Processing Mathematical Expressions -- Problems and Solutions for Markup for Mathematical Examples and Exercises -- An Annotated Corpus and a Grammar Model of Theorem Description -- A Query Language for a Metadata Framework about Mathematical Resources -- Information Retrieval in MML -- An Expert System for the Flexible Processing of XML -Based Mathematical Knowledge in a PROLOG?Environment -- Towards Collaborative Content Management and Version Control for Structured Mathematical Knowledge -- On the Integrity of a Repository of Formalized Mathematics -- A Theoretical Analysis of Hierarchical Proofs -- Comparing Mathematical Provers -- Translating Mizar for First Order Theorem Provers -- Invited Talk -- The Mathematical Semantic Web. 330 $aThis book constitutes the refereed proceedings of the Second International Conference on Mathematical Knowledge Management, MKM 2003, held in Betinoro, Italy, in February 2003.The 16 revised full papers presented together with an invited paper were carefully reviewed and selected for presentation. Among the topics addressed are digitization, representation, formalization, proof assistants, distributed libraries of mathematics, NAG library, LaTeX, MathML, mathematics markup, theorem description, query languages for mathematical metadata, mathematical information retrieval, XML-based mathematical knowledge processing, semantic Web, mathematical content management, formalized mathematics repositories, theorem proving, and proof theory. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v2594 606 $aArtificial intelligence 606 $aInformation storage and retrieval 606 $aLogic, Symbolic and mathematical 606 $aComputer science?Mathematics 606 $aDatabase management 606 $aComputer science$xMathematics 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 606 $aInformation Storage and Retrieval$3https://scigraph.springernature.com/ontologies/product-market-codes/I18032 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 606 $aSymbolic and Algebraic Manipulation$3https://scigraph.springernature.com/ontologies/product-market-codes/I17052 606 $aDatabase Management$3https://scigraph.springernature.com/ontologies/product-market-codes/I18024 606 $aComputational Mathematics and Numerical Analysis$3https://scigraph.springernature.com/ontologies/product-market-codes/M1400X 615 0$aArtificial intelligence. 615 0$aInformation storage and retrieval. 615 0$aLogic, Symbolic and mathematical. 615 0$aComputer science?Mathematics. 615 0$aDatabase management. 615 0$aComputer science$xMathematics. 615 14$aArtificial Intelligence. 615 24$aInformation Storage and Retrieval. 615 24$aMathematical Logic and Formal Languages. 615 24$aSymbolic and Algebraic Manipulation. 615 24$aDatabase Management. 615 24$aComputational Mathematics and Numerical Analysis. 676 $a510/.285 702 $aAsperti$b Andrea$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aBuchberger$b Bruno$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aDavenport$b James Harold$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aInternational Conference on Mathematical Knowledge Management 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910143881103321 996 $aMathematical Knowledge Management$9771964 997 $aUNINA