structure of qed

Konrad Slind <>
From: Konrad Slind <>
Subject: structure of qed
Message-id: <>
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.