I agreed with the organizers to lead a discussion on
Cooperation of Automated and Interactive Theorem Provers
at the workshop. In the introduction I shall report on the cooperation
experience gained in the german Schwerpunktprogramm Deduktion
(provers and people).
I shall also report on setting up an Internet mail server to provide
distant provers with natural language proof presentations.
However, there are certainly a lot of other useful things to do
concerning cooperation.
Therefore, if you have any idea on the subject - possibly even vague or
unrealistic - please, send them to
Bernd, Ingo Dahn,
Institut fuer Reine Mathematik
der Humboldt-Universitaet
Ziegelstr. 13a
D-10099 Berlin
Please, note that this is not! to start a network discussion now but only
for the benefit of the workshop. So, don't expect any comments for now.
Best regards
Ingo Dahn