Date: Thu, 18 May 95 15:10:14 +0200
From: dahn@mathematik.hu-berlin.de (Bernd Ingo Dahn)
Message-Id: <9505181310.AA26918@mathematik.hu-berlin.de>
To: qed@mcs.anl.gov
Subject: QED Workshop 2 -  Cooperation of Automated and Interactive Theorem Provers
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

This is a brainstorming request in preparation of the QED Workshop 2
in Bialystok/Poland in July.

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

	dahn@mathematik.hu-berlin.de

	 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