MKM 2005 Program
Thursday, 14. July 2005
| Time | Title | Place |
|---|---|---|
| 9:00 - 17:30 | SESAME Workshop | West Hall |
| 19:30 - ??:?? | MKM Welcome Reception | IUB Faculty Club |
Friday, 15. July 2005
The Conference will take place in Conrad Naber Lecture Hall in Reimar Lüst Hall (Admin Building)
| Time | Title | Speaker |
|---|---|---|
| 09:00 - 09:15 | Opening | the organizers |
| 09:15 - 10:15 | Session I (Fundamentals) | Chair: Manfred Kerber |
| 9:15 - 9:45 | A Proof-Theoretic Approach to Hierarchical Math Library Organization | Kamal Aboul-Hosn and Terese Damhoej Andersen |
| 9:45 - 10:15 | An Exploration in the Space of Mathematical Knowledge | Andrea Kohlhase and Michael Kohlhase |
| 10:15 - 10:45 | Coffee Break | |
| 10:45 - 12:15 | Session II (Authoring) | Chair: Paul Cairns |
| 10:45 - 11:15 | Authoring Presentation for OpenMath | Shahid Manzoor, Paul Libbrecht, Carsten Ullrich and Erica Melis |
| 11:15 - 11:45 | Translating Mathematical Vernacular into Knowledge Repositories | Adam Grabowski and Christoph Schwarzweller |
| 11:45 - 12:15 | Assisted Proof Document Authoring | David Aspinall, Christoph Lüth and Burkhart Wolff |
| 12:15 - 14:00 | Lunch | |
| 14:00 - 15:30 | Session III (Representations) | Chair: William Farmer |
| 14:00 - 14:30 | A Tough Nut for Mathematical Knowledge Management | Manfred Kerber and Martin Pollet |
| 14:30 - 15:00 | Textbook Proofs Meet Formal Logic - The Problem of Underspecification and Granularity | Serge Autexier and Armin Fiedler |
| 15:00 - 15:30 | Processing Textbook-style Matrices | Alan Sexton and Volker Sorge |
| 15:30 - 16:00 | Coffee Break | |
| 16:00 - 17:30 | Session IV (Proving) | Chair: Renaud Rioboo |
| 16:00 - 16:30 | Impasse-Driven Reasoning in Proof Planning | Andreas Meier and Erica Melis |
| 16:30 - 17:00 | A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity | Serge Autexier, Christoph Benzmueller, Dominik Dietrich, Andreas Meier and Claus-Peter Wirth |
| 17:00 - 17:30 | Literate proving: presenting and documenting formal proofs | Paul Cairns and Jeremy Gow |
| 17:30 - 18:30 | MKM business meeting | |
| 19:00 - ??:?? | Conference Dinner | |
Saturday, 16. July 2005
| Time | Title | Speaker |
|---|---|---|
| 09:00 - 10:00 | Session V (Invited Talk) | Chair: Herman Geuvers |
| 9:00 - 10:00 | The Jordan Curve Theorem, from a formal point of view | Tom Hales |
| 10:00 - 10:30 | Coffee Break | |
| 10:30 - 12:30 | Session VI (MKManagement Tools) | Chair: Tom Hales |
| 10:30 - 11:00 | Semantic Matching for Mathematical Services | William Naylor and Julian Padget |
| 11:00 - 11:30 | Label Management in Theorema | Florina Piroi, Bruno Buchberger, Camelia Rosenkranz and Tudor Jebelean |
| 11:30 - 12:00 | Mathematical Knowledge Browser with Automatic Hyperlink Detection | Koji Nakagawa and Masakazu Suzuki |
| 12:00 - 12:30 | A Database of Glyphs for OCR of Mathematical Documents | Alan Sexton and Volker Sorge |
| 12:30 - 14:00 | Lunch | |
| 14:00 - 15:30 | Session VII (Documents) | Chair: Serge Autexier |
| 14:00 - 14:30 | Toward an Object-Oriented Structure for Mathematical Text | Fairouz Kamareddine, Manuel Maarek and J. B Wells |
| 14:30 - 15:00 | Explanation in Natural Language of lambda-bar-mu-mu-tilde terms | Claudio Sacerdoti Coen |
| 15:00 - 15:30 | Engineering Mathematical Knowledge | Achim Mahnke and Jan Scheffczyk |
| 15:30 - 16:00 | Coffee Break | |
| 16:00 - 17:00 | Session VIII (MKM Case studies) | Andrzej Trybulec |
| 16:00 - 16:30 | Computational Origami of a Morley's Triangle | Tetsuo Ida, Mircea Marin and Hidekazu Takahashi |
| 16:30 - 17:00 | Designing diagrammatic catalogues of types of basic interval equation: A case study | Zenon Kulpa |
| 17:00 - 17:30 | Gröbner Bases -- Theory Refinement in the Mizar System | Christoph Schwarzweller |
Sunday, 17. July 2005
| Time | Title | Speaker |
|---|---|---|
| 09:00 - 10:00 | Session IX (Course Materials) | Tetsuo Ida |
| 9:00 - 9:30 | An Interactive Algebra Course with Formalised Proofs and Definitions | Andrea Asperti, Herman Geuvers, Iris Loeb, Lionel Mamane and Claudio Sacerdoti Coen |
| 9:30 - 10:00 | Interactive Learning and Mathematical Calculus | Arjeh M. Cohen, Hans Cuypers, Dorina Jibetean and Mark Spanbroek |
| 10:00 - 10:30 | Determining Empirical Characteristics of Mathematical Expression Use | Clare So and Stephen Watt |
| 10:30 - 11:00 | Coffee Break | |
| 11:00 - 12:30 | Session X (Migration) | Andrew Adams |
| 10:30 - 11:00 | XML-izing Mizar: making semantic processing and presentation of MML easy | Josef Urban |
| 11:00 - 11:30 | Transformations of MML Database's Elements | Robert Milewski |
| 11:30 - 12:00 | Translating a Fragment of Weak Type Theory into Type Theory with Open Terms | Georgi Jojgov |
| 12:15 - 14:00 | Lunch | |