Program of the Mathematical Knowledge Management Symposium

Heriot-Watt University, Edinburgh

25-29 November 2003

http://www.cedar-forest.org/forest/events/mkm-symposium03/


 
 

Schedule

http://www.macs.hw.ac.uk/~fairouz/mkm-symposium03/program.html
 
 
 

Tuesday, 25 November 2003

Room 1.27

     13:00 - 14:00         REGISTRATION


Chair: Fairouz Kamareddine
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




Morning Session Chairs: Michiel Hazewinkel and Chris Benzmueller
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


Afternoon Session Chairs: James Davenport and Tudor Jebelean
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




Morning Session Chair: Mike Dewar
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


Afternoon Session Chair: Erica Melis and Henk Barendregt
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




Morning Session Chairs: Andrea Asperti and Manfred Kerber
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


Afternoon Session Chair: Paul Cairns
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





Morning Session Chair: Roy McCasland

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.