If we are to make QED a public resource, let's keep in mind recent
advances in distributed database technology (such as WWW and mosaic).
It would be really interesting to find WWW resources besides the
weather and the latest Dr. Fun Cartoon. (You can also find tangos, by
the way and some really beautiful, albeit risque' pictures of tango
dancers).
Javier
Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id KAA23797 for qed-out; Wed, 1 Nov 1995 10:24:49 -0600
Received: from catseye.idbsu.edu (catseye.idbsu.edu [132.178.200.125]) by antares.mcs.anl.gov (8.6.10/8.6.10) with SMTP
id KAA23792 for <qed@mcs.anl.gov>; Wed, 1 Nov 1995 10:24:39 -0600
Message-Id: <199511011624.KAA23792@antares.mcs.anl.gov>
Received: by catseye.idbsu.edu
(1.38.193.4/16.2) id AA08775; Wed, 1 Nov 1995 09:32:57 -0700
Date: Wed, 1 Nov 1995 09:32:57 -0700
From: Randall Holmes <holmes@catseye.idbsu.edu>
To: qed@mcs.anl.gov
Subject: PRA implementation
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
There is some more material about my proposed implementation of a
"root logic" equivalent in strength to PRA (a theory of binary trees)
on my WWW page. Follow the link to QED, then to the meta-logic
proposal, then to "something more concrete". This is still very much
draft material; it is lacking both proofs of equivalence with PRA and
a report on experience with actual implementation under my prover.
The opinions expressed | --Sincerely, M. Randall Holmes
above are not the official | Math. Dept., Boise State Univ.
opinions of any person | holmes@math.idbsu.edu
or institution. | http://math.idbsu.edu/faculty/holmes.html