LEADER 04657nam 22008295 450 001 996465650803316 005 20200705235308.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(EXLCZ)991000000000211928 100 $a20121227d2003 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aMathematical Knowledge Management$b[electronic resource] $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 $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. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v2594 606 $aArtificial intelligence 606 $aInformation storage and retrieval 606 $aMathematical logic 606 $aComputer science?Mathematics 606 $aDatabase management 606 $aComputer mathematics 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$aMathematical logic. 615 0$aComputer science?Mathematics. 615 0$aDatabase management. 615 0$aComputer mathematics. 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 $a996465650803316 996 $aMathematical Knowledge Management$9771964 997 $aUNISA