Schedule
http://www.macs.hw.ac.uk/~fairouz/mkm-symposium03/program.html
Tuesday, 25 November 2003
Room 1.27
13:00 - 14:00
REGISTRATION
| 14:00 - 15:00 | Keynote speech
Why mathematical knowledgement and what could it be? (abstract, slides.pdf) Michiel Hazewinkel (Amsterdam, NL) |
| 15:00 - 15:30 |  BREAK |
| 15:30-16:30 | Invited Lecture
OMEGA --- From Proof Planning towards Mathematical Knowledge Management (abstract.ps, slides.pdf) Serge Autexier and Christoph Benzmueller (Saarbrucken, Germany) |
| 16:30 - 17:30 | Invited Lecture
The Mizar project (abstract) Andrzej Trybulec (Bialystok, Poland) |
| 18:30 | Closed meeting for consortium and deliverables |
Wednesday, 26 November 2003
Room 1.27 in the morning, 1.83 in the afternoon
| 9:00 - 10:00 | Keynote Speech
Steps toward a World Wide Digital Library of Formal Mathematics(abstract, slides.ppt) Bob Constable (Cornell, USA) |
| 10:00 - 10:30 |  BREAK |
| 10:30 - 11.30 | Invited lecture
Mathematical Knowldge Management and Theorema Tudor Jebelean (RISC-Linz, Austria) |
| 11:30 - 12:00 |
Algorithm Synthesis by Lazy Thinking: Examples and Implementation in Theorema
Buchberger and Craciun |
12.00 - 14.00
LUNCH
| 14:00 - 15:00 | Invited lecture
Putting Mathematics onto the Semantic Web (abstract, slides.pdf) Mike Dewar (NAG,UK) |
| 15:00 - 15.30 | BREAK |
| Accepted talks | 15.30 - 18.00 |
| 15:30 - 16.00 |
LogiWeb
Klaus Grue |
| 16:00 - 16.30 |
Adapting mainstream editors for semantic authoring of mathematics
Goguadze and Gonzalez |
| 16:30 - 17.00 | BREAK |
| 17:00 - 17.30 |
Deduction and presentation in rowLog (slides.pdf)
Marin and Piroi |
| 17:30 - 18.00 |
Assertion level proof representation with under-specification(slides.pdf)
Autexier, Benzmuller, Fiedler, Horacek and Vo |
19.30
SOCIAL BANQUET
Thursday, 27 November 2003
Room 1.27
| 9:00 - 10:00 | Keynote Speech
Computational Mathematics James Davenport (Bath, UK) |
| 10.00 - 10.30 | BREAK |
| 10:30 - 11:30 | Invited lecture
ActiveMath: Personalization, Active Learning, OMDoc and more Erica Melis (Saarbrucken, Germany) |
| 11:30 - 12:30 | Invited lecture
OMDoc - The Representation Format for Mathematical Knowledge(abstract, talk.ps) Michael Kohlhase (presented by George Goguadze) (Bremen and Saarbrucken, Germany) |
12.30 - 14.00
LUNCH
| 14:00 - 15:00 | Invited lecture
The Science of Equality: Some Statistical Considerations on the Coq Library Andrea Asperti (Bologna, Italy) |
| 15.00 - 15:30 | BREAK |
| 15.30 - 18.00 Accepted talks |
| 15:30 - 16.00 |
Using and Parsing the Mizar Language
Paul Cairns and Jeremy Gow |
| 16:00 - 16.30 |
MathLang: experience-driven development of a new
mathematical language
(abstract,slides.ps)
Kamareddine, Maarek and Wells |
| 16:30 - 17.00 |  BREAK |
| 17:00 - 17.30 |
A calculus of tactics and its operations semantics
G. Jojgov |
| 17:30 - 18.00 |
faithfully reflecting the structure of Informal Mathematical proofs into formal theories
Jojgov, Nederpelt and Scheffer |
| 19:00 | Closed meeting for MKM NET |
Friday, 28 November 2003
Room 1.27
| 9:00 - 10:00 | Keynote Speech
Proposal for a machine & human refereed library of mathematics Henk Barendregt (Nijmegen, NL) |
| 10.00 - 10.30 | BREAK |
| 10:30 - 11.30 | Invited lecture
Searching Mathematical Content for Education Ingo Dahn (Germany) |
| 11:30 - 12:00 |
Ordered set in Isabelle/HOL
Kobayashi and Suzuki |
12.00 - 14.00
LUNCH
| 14:00 - 15:00 | Invited lecture
Mathematical Formula Recognition Alan Sexton (Birmingham, UK) |
| 15:00 - 15.30 | BREAK |
| 15:30-16:30 | Invited Lecture
FoC and the external world Renaud Rioboo (Paris, France) |
| 16:30 - 17:00 | Invited Lecture
Building a Tool for Teaching Mathematical Logic (abstract, slides.pdf) Manfred Kerber (Birmingham, UK) |
| 17:00 - 17:30 | Invited Lecture
Logosphere -- A Digital Library of Formal Proof Content + Meaning Carsten Schuermann (Yale, USA) |
Saturday, 29 November 2003
Room 1.27
| 9:00 - 10:00 | Keynote Speech
Recollecting the Automath project (abstract, slides.pdf, extra slides.pdf ) N.G. de Bruijn (Eindhoven, NL) |
| 10:00 - 10:30 | BREAK |
| Accepted talks | 10.30 - 12.00 |
| 10:30 - 11.00 |
Mathematical, Interactive exercises Generation from static documents
(slides.ppt)
Mavrikis and Gonzalez |
| 11:00 - 11.30 |
A survey of syntactically defined decidable clausal classes
Lilia Georgiva |
| 11:30 - 12.00 |
Mathematical Knowledge Browser
Nakagawa and Suzuki |
| 12:00 - 17:00 | Closed meeting for MKM NET |
12.00
END of Symposium and START of MKM NET planning CLOSED meeting
Fairouz Kamareddine
URL: http://www.cedar-forest.org/forest/events/mkm-symposium03/
Last modified: Wednesday 12 November 2003.