QED Workshop II
Warsaw, July 20 - 22, 1995
AGENDA: We plan to run the workshop us a series of one-hour sessions.
A session consists of 20 - 30 min. introductory talk, followed
by discussion dedicated to specific topic.
Thursday, July 20
10:00 - 11:00 Andrzej Trybulec - Computer reconstruction of
mathematical technology,
11:00 - 12:00 Paul Jackson - Can we agreeably resolve the tension
between type theorists (constructivists,
de Bruijn, Martin Lof, Constable) and
the classical mathematicians?
12:00 - 13:00 Martin Strecker - The organization of a data base of
mathematical knowledge,
13:30 - 14:15 lunch in "Parkowa"
14:30 - 15:30 Randall Holmes - Indeterminateness,
15:30 - 16:30 Manfred Kerber - Possible use of already formalized
mathematical knowledge,
16:30 - 17:30 John Harrison - Reflection: practically necessary
or not,
18:00 - departure to the Old City by bus, dinner at Karczma (Inn)
Friday, July 21
10:00 - 11:00 Javier Thayer - Formalized Analysis,
11:00 - 12:00 Peter White - Mathematical synthesis,
12:00 - 13:00 Andrzej Trybulec - Syntax vs. semantics,
13:30 - 14:30 lunch in "Parkowa"
15:00 - 16:00 John McCarthy - Heavy duty set theory,
16:00 - 18:00 panel discussion
19:00 - cocktail banquet in "Parkowa"
Saturday, July 22
10:00 - 11:00 Piotr Rudnicki - To type or not to type,
11:00 - 12:00 Bernd Ingo Dahn - Cooperation of automated and
interactive theorem provers,
12:00 - 13:00 Deepak Kapur - What are the connections, interrela-
tions, and antipathies between proof
checking and automatic theorem proving?
13:30 - 14:30 lunch in "Parkowa"
14:30 - 15:30 Grzegorz Bancerek - Mizar proof of the mutilated
checkerboard problem,
15:30 - 16:30 Manfred Kerber - Why we are needed by mathematics,
16:30 - 17:30 General discussion about QED future.
Workshop ends.
-- Roman Matuszewski
(Workshop Chairman)