Conferences on Intelligent Computer Mathematics - Birmingham 2008
7th International Conference on
Mathematical Knowledge Management

MKM 2008

Birmingham, UK, 28-30 July 2008

Preliminary Conference Program

Monday, 28 July 2008

Session 1: Invited Talk
(Chair: Masakazu Suzuki, room: 1)

09:30-10:30: Thierry Bouche:
Digital mathematics libraries: The good, the bad, the ugly


10:30-11:00: Coffee Break


Session 2: Repositories
(Chair: Thierry Bouche, room: 1)

11:00-11:30: Heinrich Stamerjohanns, Michael Kohlhase:
Transforming the arXiv to XML

11:30-12:00: Radim Řehůřek, Petr Sojka:
Automated Classification and Categorization of Mathematical Knowledge

12:00-12:30: Freek Wiedijk:
Statistics on digital libraries of mathematics


12:30-14:30: Lunch


Session 3: Formalized Mathematics Documents
(Chair: Bill Farmer, room: 1)

14:00-14:30: Konstantin Verchinine, Alexander Lyaletski, Andrei Paskevich, Anatoly Anisimov:
On correctness of mathematical texts from a logical and practical point of view

14:30-15:00: Dominik Dietrich, Ewaryst Schulz, Marc Wagner:
Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors

15:00-15:30: Stefan Berghofer, Makarius Wenzel:
Logic-free reasoning in Isabelle/Isar


15:30-16:00: Coffee Break


Session 4: Mathematical Notation
(Chair: Alan Sexton, room: 1)

16:00-16:30: Akio Fujiyoshi, Masakazu Suzuki, Seiichi Uchida:
Verification of Mathematical Formulae Based on a Combination of Context-Free Grammar and Tree Grammar

16:30-17:00: Michael Kohlhase, Christine Müller, Florian Rabe:
Notations for Living Mathematical Documents

17:00-17:30: Petr Sojka and Jiří Rákosník:
From pixels and minds to the mathematical knowledge in digital library


System Demonstrations
(Chair: Manfred Kerber, room: 2 and 3)

17:30-18:15: Konstantin Verchinine, Alexander Lyaletski, Andrei Paskevich, Anatoly Anisimov:
Demonstration: On correctness of mathematical texts from a logical and practical point of view

17:30-18:15: Dominik Dietrich, Ewaryst Schulz, Marc Wagner:
Demonstration: Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors


19:00-20:00: Reception


Tuesday, 29 July 2008

Session 5: Invited Talk
(Chair: Serge Autexier, room: 1)

09:30-10:30: Alan Bundy:
Automating Signature Evolution in Logical Theories


10:30-11:00: Coffee Break


Session 6: Representations I
(Chair: Bruce Miller, room: 1)

11:00-11:30: Joseph Collins:
A Mathematical Type for Physical Variables

11:30-12:00: James Davenport, Jonathan Stratford:
Unit Knowledge Management

12:00-12:30: Aaron Sloman:
Kantian Philosophy of Mathematics and Young Robots


12:30-14:00: Lunch


Session 7: Representations II
(Chair: Tetsuo Ida, room: 1)

14:00-14:30: Manfred Kerber:
Normalization Issues in Mathematical Representations

14:30-15:00: John Howse, Gem Stapleton:
Visual Mathematics: Diagrammatic Formalization and Proof

15:00-15:30: Jónathan Heras, Vico Pascual, Julio Rubio:
Mediated Access to Symbolic Computation Systems


15:30-16:00: Coffee Break


Session 8: Search
(Chair: Paul Libbrecht, room: 1)

16:00-16:30: Bruce Miller, Abdou Youssef:
Augmenting Presentation MathML for Search

16:30-17:00: Michael Kohlhase, Stefan Anca, Constantin Jucovschi, Alberto González Palomo and Ioan Sucan:
System demonstration: MathWebSearch 0.4, A Semantic Search Engine for Mathematics


Session 9: Business meeting
(Room: 1)

17:00-18:00: Business meeting


19:00-21:00: Banquet


Wednesday, 30 July 2008

Session 10: eLearning
(Chair: Michael Kohlhase, room: 1)

09:30-10:00: Paul Libbrecht, Cyrille Desmoulins, Christian Mercat, Colette Laborde, Michael Dietrich, Maxim Hendriks:
Cross-Curriculum Search for Intergeo

10:00-10:30: Bastiaan Heeren, Johan Jeuring, Arthur Leeuwen, van, Alex Gerdes:
Specifying Strategies for Exercises


10:30-11:00: Coffee Break


Session 11: Proofs
(Chair: Bengt Nordström, room: 1)

11:00-11:30: David Aspinall, Ewen Denney, Christoph Lüth:
A Tactic Language for Hiproofs

11:30-12:00: Stefan Hetzl, Alexander Leitsch, Daniel Weller, Bruno Woltzenlogel Paleo:
Herbrand Sequent Extraction

12:00: Closing Remarks