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