Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date:
Received: from antares.mcs.anl.gov (actually antares9.mcs.anl.gov !OR! qed-owner@mcs.anl.gov)
          by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk;
          Mon, 9 Aug 1993 15:46:49 +0100
Received: by antares.mcs.anl.gov id AA27389 (5.65c/IDA-1.4.4 for qed-outgoing);
          Mon, 9 Aug 1993 09:34:14 -0500
Received: from mail.Germany.EU.net by antares.mcs.anl.gov with SMTP
          id AA27382 (5.65c/IDA-1.4.4 for <qed@mcs.anl.gov>);
          Mon, 9 Aug 1993 09:34:07 -0500
Received: by mail.Germany.EU.net(EUnetD-2.3.0.g) via EUnet id GM06812;
          Mon, 9 Aug 1993 16:31:50 +0200
Received: from hubinf.informatik.hu-berlin.de by hp832.informatik.hu-berlin.de
          with SMTP (15.11/15.6) id AA17629; Mon, 9 Aug 93 13:48:22 mes
Received: from noether.hu-berlin.de by hubinf (4.1/SMI-4.1) id AA19189;
          Mon, 9 Aug 93 13:51:49 +0200
Date: Mon, 9 Aug 93 13:51:49 +0200
From: dahn@hubinf.informatik.hu-berlin.de (Dahn)
Message-Id: <9308091151.AA19189@hubinf>
To: qed@mcs.anl.gov
Subject: Re: QED-like Efforts
Sender: qed-owner@mcs.anl.gov

Certainly there will be numeruous proof systems, calculi, philosophies etc. and
people like to stay with the things they know and they can efficiently work
with. So, why not - in a first phase - encourage people to verify in their own
system the stuff (set theory, universal algebra, syntactic properties)
necessary to verify the completeness of other systems? Then a verification in
any of the verified systems would be as good as a verification in the original
system.

Bernd, Ingo Dahn