Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.2 9/18/84; site wdl1.UUCP
Path: utzoo!watmath!clyde!burl!ulysses!bellcore!decvax!decwrl!sun!wdl1!jbn
From: jbn@wdl1.UUCP
Newsgroups: net.ai
Subject: Re: Re: A halting problem: a meaty respo
Message-ID: <969@wdl1.UUCP>
Date: Thu, 30-Jan-86 21:08:55 EST
Article-I.D.: wdl1.969
Posted: Thu Jan 30 21:08:55 1986
Date-Received: Sat, 1-Feb-86 06:03:43 EST
Sender: notes@wdl1.UUCP
Organization: Ford Aerospace, Western Development Laboratories
Lines: 17
Nf-ID: #R:kestrel:-437400:wdl1:91300002:000:751
Nf-From: wdl1!jbn    Jan 30 13:15:00 1986


      If we're going to argue foundations of mathematics, I have to put in
a plug for Bob Boyer and Jay Moore's continuing effort to build up
mathematics from a brutally simple constructive base, using an automatic
theorem prover to do the grunt work.  See Boyer and Moore, ``A 
Computational Logic'', Academic Press, 1979.  Their approach is based
on recursive function theory and uses a pure-Lisp notation.  I've spent
many happy hours trying to convince their prover that something I wanted
to prove is correct.  I'm submitting a paper to JACM in which I show that
the generally accepted axioms for arrays (using "select" and "store")
are consistent, using constructive machine proofs.

				John Nagle
				League of the Militant Constructivists