4. MKM 2005: Bremen, Germany

Foundations

• Kamal Aboul-Hosn, Terese Andersen:
  A Proof-Theoretic Approach to Hierarchical Math Library Organization. 1-16
  
• Andrea Kohlhase, Michael Kohlhase:
  An Exploration in the Space of Mathematical Knowledge. 17-32
  

Authoring

• Shahid Manzoor, Paul Libbrecht, Carsten Ullrich, Erica Melis:
  Authoring Presentation for OpenMath. 33-48
  
• Adam Grabowski, Christoph Schwarzweller:
  Translating Mathematical Vernacular into Knowledge Repositories. 49-64
  
• David Aspinall, Christoph Lüth, Burkhart Wolff:
  Assisted Proof Document Authoring. 65-80
  

Representations

• Manfred Kerber, Martin Pollet:
  A Tough Nut for Mathematical Knowledge Management. 81-95
  
• Serge Autexier, Armin Fiedler:
  Textbook Proofs Meet Formal Logic - The Problem of Underspecification and Granularity. 96-110
  
• Alan P. Sexton, Volker Sorge:
  Processing Textbook-Style Matrices. 111-125
  

Proving

• Serge Autexier, Christoph Benzmüller, Dominik Dietrich, Andreas Meier, Claus-Peter Wirth:
  A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity. 126-142
  
• Andreas Meier, Erica Melis:
  Impasse-Driven Reasoning in Proof Planning. 143-158
  
• Paul A. Cairns, Jeremy Gow:
  Literate Proving: Presenting and Documenting Formal Proofs. 159-173
  

MKManagement Tools

• William Naylor, Julian A. Padget:
  Semantic Matching for Mathematical Services. 174-189
  
• Koji Nakagawa, Masakazu Suzuki:
  Mathematical Knowledge Browser with Automatic Hyperlink Detection. 190-202
  
• Alan P. Sexton, Volker Sorge:
  A Database of Glyphs for OCR of Mathematical Documents. 203-216
  

Documents

• Fairouz Kamareddine, Manuel Maarek, J. B. Wells:
  Toward an Object-Oriented Structure for Mathematical Text. 217-233
  
• Claudio Sacerdoti Coen:
  Explanation in Natural Language of lamda-µµ-Terms. 234-249
  
• Achim Mahnke, Jan Scheffczyk:
  Engineering Mathematical Knowledge. 250-266
  

MKM Case Studies

• Tetsuo Ida, Hidekazu Takahashi, Mircea Marin:
  Computational Origami of a Morley's Triangle. 267-282
  
• Zenon Kulpa:
  Designing Diagrammatic Catalogues of Types of Basic Interval Equation: A Case Study. 283-298
  
• Christoph Schwarzweller:
  Gröbner Bases - Theory Refinement in the Mizar System. 299-314
  

Course Materials

• Andrea Asperti, Herman Geuvers, Iris Loeb, Lionel Elie Mamane, Claudio Sacerdoti Coen:
  An Interactive Algebra Course with Formalised Proofs and Definitions. 315-329
  
• Arjeh M. Cohen, Hans Cuypers, Dorina Jibetean, Mark Spanbroek:
  Interactive Learning and Mathematical Calculus. 330-345
  

Migration

• Josef Urban:
  XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy. 346-360
  
• Clare M. So, Stephen M. Watt:
  Determining Empirical Characteristics of Mathematical Expression Use. 361-375
  
• Robert Milewski:
  Transformations of MML Database's Elements. 376-388
  
• Gueorgui I. Jojgov:
  Translating a Fragment of Weak Type Theory into Type Theory with Open Terms. 389-403