LEADER 04650nam 22008295 450 001 9910767556503321 005 20251226204004.0 010 $a3-540-37106-0 024 7 $a10.1007/11812289 035 $a(CKB)1000000000283920 035 $a(SSID)ssj0000318813 035 $a(PQKBManifestationID)11254479 035 $a(PQKBTitleCode)TC0000318813 035 $a(PQKBWorkID)10336060 035 $a(PQKB)10919277 035 $a(DE-He213)978-3-540-37106-9 035 $a(MiAaPQ)EBC3068104 035 $a(PPN)123137179 035 $a(BIP)34164174 035 $a(BIP)13552778 035 $a(EXLCZ)991000000000283920 100 $a20100301d2006 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aMathematical Knowledge Management $e5th International Conference, MKM 2006, Wokingham, UK, August 11-12, 2006, Proceedings /$fedited by Jonathan Borwein, William M. Farmer 205 $a1st ed. 2006. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2006. 215 $a1 online resource (VIII, 295 p.) 225 1 $aLecture Notes in Artificial Intelligence,$x2945-9141 ;$v4108 300 $aBibliographic Level Mode of Issuance: Monograph 311 08$a3-540-37104-4 320 $aIncludes bibliographical references and index. 327 $aInvited Talks -- The Omega Number: Irreducible Complexity in Pure Math -- Roles of Math Search in Mathematics -- Contributed Papers -- Structured Induction Proofs in Isabelle/Isar -- Interpretation of Locales in Isabelle: Theories and Proof Contexts -- A Dynamic Poincaré Principle -- A Proof-Theoretic Approach to Tactics -- A Formal Correspondence Between OMDoc with Alternative Proofs and the -Calculus -- Proof Transformation by CERES -- Synthesizing Proof Planning Methods and ?-Ants Agents from Mathematical Knowledge -- Verifying and Invalidating Textbook Proofs Using Scunak -- Capturing Abstract Matrices from Paper -- Towards a Parser for Mathematical Formula Recognition -- Stochastic Modelling of Scientific Terms Distribution in Publications -- Capturing the Content of Physics: Systems, Observables, and Experiments -- Communities of Practice in MKM: An Extensional Model -- From Notation to Semantics: There and Back Again -- Managing Informal Mathematical Knowledge: Techniques from Informal Logic -- From Untyped to Polymorphically Typed Objects in Mathematical Web Services -- Managing Automatically Formed Mathematical Theories -- Authoring LeActiveMath Calculus Content -- Information Retrieval and Rendering with MML Query -- Integrating Dynamic Geometry Software, Deduction Systems, and Theorem Repositories. 330 $aThis book constitutes the refereed proceedings of the 5th International Conference on Mathematical Knowledge Management, MKM 2006, held in Wokingham, UK, August 2006. The book presents 22 revised full papers. Coverage extends to the mathematical knowledge management at the intersection of mathematics, computer science, library science, and scientific publishing. The papers are organized in topical sections on proof representations, proof processing, knowledge extraction, knowledge representation, as well as systems and tools. 410 0$aLecture Notes in Artificial Intelligence,$x2945-9141 ;$v4108 606 $aArtificial intelligence 606 $aInformation storage and retrieval systems 606 $aApplication software 606 $aDatabase management 606 $aComputer networks 606 $aMathematics 606 $aArtificial Intelligence 606 $aInformation Storage and Retrieval 606 $aComputer and Information Systems Applications 606 $aDatabase Management 606 $aComputer Communication Networks 606 $aMathematics 615 0$aArtificial intelligence. 615 0$aInformation storage and retrieval systems. 615 0$aApplication software. 615 0$aDatabase management. 615 0$aComputer networks. 615 0$aMathematics. 615 14$aArtificial Intelligence. 615 24$aInformation Storage and Retrieval. 615 24$aComputer and Information Systems Applications. 615 24$aDatabase Management. 615 24$aComputer Communication Networks. 615 24$aMathematics. 676 $a511.3/6028563 701 $aBorwein$b Jonathan M$055373 701 $aFarmer$b William Michael$01357617 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910767556503321 996 $aMathematical knowledge management$94201972 997 $aUNINA