Mathematical Knowledge Management: Third International Conference, MKM 2004, Białowieża, Poland, September 19-21, 2004. Proceedings

Andrew A. Adams, James H. Davenport (auth.), Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec (eds.)3540230297, 9783540230298, 9783540278184

This book constitutes the refereed proceedings of the Third International Conference on Mathematical Knowledge Management, MKM 2004, held in Bialowieza, Poland, in September 2004.

The 27 revised full papers presented were carefully reviewed and selected from 48 submissions. Among the topics addressed are mathematics retrieval, formalizing mathematics, formal mathematics, digital mathematical libraries, semantic Web, knowledge repositories, mathematical knowledge representation, theorem proving systems, OWL, proof verification, formal representation, mathematical formulae processing, and the OpenMath project.

---

Table of contents :
Front Matter….Pages –
Copyright Issues for MKM….Pages 1-16
Efficient Retrieval of Mathematical Statements….Pages 17-31
Formalizing Set Theory as it Is Actually Used….Pages 32-43
Integrated Semantic Browsing of the Mizar Mathematical Library for Authoring Mizar Articles….Pages 44-57
Informalising Formal Mathematics: Searching the Mizar Library with Latent Semantics….Pages 58-72
Mathematical Service Matching Using Description Logic and OWL….Pages 73-87
C-CoRN, the Constructive Coq Repository at Nijmegen….Pages 88-103
Classifying Differential Equations on the Web….Pages 104-115
Managing Heterogeneous Theories within a Mathematical Knowledge Repository….Pages 116-129
Rough Concept Analysis – Theory Development in the Mizar System….Pages 130-144
A Path to Faithful Formalizations of Mathematics….Pages 145-159
Flexible Encoding of Mathematics on the Computer….Pages 160-174
CPoint : Dissolving the Author’s Dilemma….Pages 175-189
On Diagrammatic Representation of Mathematical Knowledge….Pages 190-204
Predicate Logic with Sequence Variables and Sequence Function Symbols….Pages 205-219
A Graph-Based Approach Towards Discerning Inherent Structures in a Digital Library of Formal Mathematics….Pages 220-235
Theorem Proving and Proof Verification in the System SAD….Pages 236-250
Adaptive Access to a Proof Planner….Pages 251-264
Modeling Interactivity for Mathematics Learning by Demonstration….Pages 265-275
Extraction of Logical Structure from Articles in Mathematics….Pages 276-289
Improving Mizar Texts with Properties and Requirements ….Pages 290-301
An Investigation on the Dynamics of Direct-Manipulation Editors for Mathematics….Pages 302-316
Intuitive and Formal Representations: The Case of Matrices….Pages 317-331
Mathematical Libraries as Proof Assistant Environments….Pages 332-346
Efficient Ambiguous Parsing of Mathematical Formulae….Pages 347-362
An Architecture for Distributed Mathematical Web Services….Pages 363-377
The Categorial Type of OpenMath Objects….Pages 378-392
Back Matter….Pages –