Friday, 15. July 2005

Time	        Title/Speaker	                                                                      
09:00 - 09:15 	Opening
09:15 - 10:15 	Session I 	
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) 	
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) 	
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) 	

16:00 - 16:30 	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
16:30 - 17:00 	Impasse-Driven Reasoning in Proof Planning 	
                Andreas Meier and Erica Melis
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) 	
9:15 - 9:45 	The Jordan Curve Theorem, from a formal point of view 	
                Tom Hales

9:45 - 10:30 	Coffee Break

10:30 - 12:30 	Session VI (MKManagement Tools) 	
10:30 - 11:00 	Semantic Matching for Mathematical Services 	
                William Naylor and Julian Padget
11:00 - 11:30 	Organisational Tools for MKM 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) 	
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 	Towards Consistent Mathematical Documents 	
                Achim Mahnke and Jan Scheffczyk

15:30 - 16:00 	Coffee Break

16:00 - 17:00 	Session VIII (MKM Case studies) 	
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) 	
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 - 11:00 	Coffee Break

11:00 - 12:30 	Session X (Migration) 	
10:30 - 11:00 	XML-izing Mizar: making semantic processing and presentation of MML easy 	
                Josef Urban
11:00 - 11:30 	Determining Empirical Characteristics of Mathematical Expression Use 	
                Clare So and Stephen Watt
11:30 - 12:00 	Transformations of MML Database's Elements 	
                Robert Milewski
12:00 - 12:30 	Translating a Fragment of Weak Type Theory into Type Theory with Open Terms 	
                Georgi Jojgov
12:15 - 14:00 	Lunch