jbn@wdl1.UUCP (01/31/86)
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