Mathematical Knowledge Management

1. Front Matter

   PDF

2. Session I: Foundations

   1. A Proof-Theoretic Approach to Hierarchical Math Library Organization

      • Kamal Aboul-Hosn, Terese Damhøj Andersen

      Pages 1-16

   2. An Exploration in the Space of Mathematical Knowledge

      • Andrea Kohlhase, Michael Kohlhase

      Pages 17-32

3. Session II: Authoring

   1. Authoring Presentation for openmath

      • Shahid Manzoor, Paul Libbrecht, Carsten Ullrich, Erica Melis

      Pages 33-48

   2. Translating Mathematical Vernacular into Knowledge Repositories

      • Adam Grabowski, Christoph Schwarzweller

      Pages 49-64

   3. Assisted Proof Document Authoring

      • David Aspinall, Christoph Lüth, Burkhart Wolff

      Pages 65-80

4. Session III: Representations

   1. A Tough Nut for Mathematical Knowledge Management

      • Manfred Kerber, Martin Pollet

      Pages 81-95

   2. Textbook Proofs Meet Formal Logic – The Problem of Underspecification and Granularity

      • Serge Autexier, Armin Fiedler

      Pages 96-110

   3. Processing Textbook-Style Matrices

      • Alan Sexton, Volker Sorge

      Pages 111-125

5. Session IV: Proving

   1. A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity

      • Serge Autexier, Christoph Benzmüller, Dominik Dietrich, Andreas Meier, Claus-Peter Wirth

      Pages 126-142

   2. Impasse-Driven Reasoning in Proof Planning

      • Andreas Meier, Erica Melis

      Pages 143-158

   3. Literate Proving: Presenting and Documenting Formal Proofs

      • Paul Cairns, Jeremy Gow

      Pages 159-173

6. Session V: MKManagement Tools

   1. Semantic Matching for Mathematical Services

      • William Naylor, Julian Padget

      Pages 174-189

   2. Mathematical Knowledge Browser with Automatic Hyperlink Detection

      • Koji Nakagawa, Masakazu Suzuki

      Pages 190-202

   3. A Database of Glyphs for OCR of Mathematical Documents

      • Alan Sexton, Volker Sorge

      Pages 203-216

7. Session VI: Documents

   1. Toward an Object-Oriented Structure for Mathematical Text

      • Fairouz Kamareddine, Manuel Maarek, J. B. Wells

      Pages 217-233

   2. Explanation in Natural Language of λ̄μμ͂-Terms

      • Claudio Sacerdoti Coen

      Pages 234-249

   3. Engineering Mathematical Knowledge

      • Achim Mahnke, Jan Scheffczyk

      Pages 250-266

8. Session VII: MKM Case Studies

   1. Computational Origami of a Morley’s Triangle

      • Tetsuo Ida, Hidekazu Takahashi, Mircea Marin

      Pages 267-282

   2. Designing Diagrammatic Catalogues of Types of Basic Interval Equation: A Case Study

      • Zenon Kulpa

      Pages 283-298

This 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.

• Algebra
• automated theorem proving
• e-learning
• equation
• formal logic
• formal mathematics
• interactive algebra
• knowledge management
• latex
• learning
• mathematical encoding
• mathematical knowledge management
• proof
• proving
• theorem

• Computer Science, Jacobs University Bremen,  

  Michael Kohlhase

Policies and ethics