structure of qed

• Mail folder: QED
• Next message: John Harrison: "Incentive to write proofs"
• Previous message: Konrad Slind: "Why Mathematical System Modeling Needs the Mathematics of Analysis"

From: Konrad Slind <slind@informatik.tu-muenchen.de>
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
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.