Date: Tue, 15 Aug 95 09:21:14 +0200
From: dahn@mathematik.hu-berlin.de (Bernd Ingo Dahn)
Message-Id: <9508150721.AA01639@mathematik.hu-berlin.de>
To: qed@mcs.anl.gov
Subject: Re: Hierarchy of theorem provers
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

I don't think that QED will develop in a linear fashion. E. g. many useful and QED-related things can be done with theorem provers for typed languages and I don't understand why these should be forced to include Heavy Duty Set Theory.

QED should urge systems to become more cooperative so that e. g. theories, formulas, proofs are reusable (which only in the most optimistic case means 'translatable'). When this has been achieved, we may examine the graph of connections that has emerged and classify its nodes.

Certainly, systems that get their proofs passed through the most tough basic proof checkers will be especially honored. This will - among others - strengthen the path from Typed Theorem Provers through Heavy Duty Theorem Provers to Basic Theorem Provers.

Ingo Dahn