Return-Path: Delivery-Date: Received: from antares.mcs.anl.gov (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Sat, 24 Apr 1993 02:15:31 +0100 Received: by antares.mcs.anl.gov id AA02424 (5.65c/IDA-1.4.4 for qed-outgoing); Fri, 23 Apr 1993 19:59:34 -0500 Received: from tuminfo2.informatik.tu-muenchen.de by antares.mcs.anl.gov with SMTP id AA02415 (5.65c/IDA-1.4.4 for ); Fri, 23 Apr 1993 19:59:21 -0500 Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <57668>; Sat, 24 Apr 1993 02:59:11 +0200 Received: by sunbroy14.informatik.tu-muenchen.de id <8079>; Sat, 24 Apr 1993 02:58:49 +0200 From: Konrad Slind To: qed@mcs.anl.gov Subject: structure of qed Message-Id: <93Apr24.025849met_dst.8079@sunbroy14.informatik.tu-muenchen.de> Date: Sat, 24 Apr 1993 02:58:36 +0200 Sender: qed-owner@mcs.anl.gov Precedence: bulk The QED manifesto does make a valid point about the atrocious state of sharing information between theorem proving systems. Consider this as a network topology problem. The QED proposal amounts to a star network, with the root logic in the middle. This requires agreeing on a root logic. What about having a ring network? Then there's no need for a root logic; all a theorem proving system needs to do to join the network is to be able to handle the "packets" (formulas and proofs) of one member of the network and ensure that its own output packets are digestible by its downstream neighbour. Konrad.