4. MKM 2005: Bremen, Germany

Michael Kohlhase (Ed.): Mathematical Knowledge Management, 4th International Conference, MKM 2005, Bremen, Germany, July 15-17, 2005, Revised Selected Papers. Lecture Notes in Computer Science 3863 Springer 2006, ISBN 3-540-31430-X BibTeX

Foundations

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

Authoring

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

Representations

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

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
Electronic Edition (link) BibTeX
Andreas Meier, Erica Melis:
Impasse-Driven Reasoning in Proof Planning. 143-158
Electronic Edition (link) BibTeX
Paul A. Cairns, Jeremy Gow:
Literate Proving: Presenting and Documenting Formal Proofs. 159-173
Electronic Edition (link) BibTeX

MKManagement Tools

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

Documents

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

MKM Case Studies

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

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
Electronic Edition (link) BibTeX
Arjeh M. Cohen, Hans Cuypers, Dorina Jibetean, Mark Spanbroek:
Interactive Learning and Mathematical Calculus. 330-345
Electronic Edition (link) BibTeX

Migration

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