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

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

Last update Fri May 25 08:27:10 2012 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page