FOM: Re: Your automated prover

[holmes@catseye.idbsu.edu]

Dear Joe (cc FOM list),

There is a link to my home page in my signature file, and that is a
place to start.  But a more direct link to the prover project is

http://math.idbsu.edu/~holmes/proverpage.html

This is the main page for the current version of the prover, and I just
checked that this is the correct address.  One can actually download the
prover itself from there and get the current theory scripts, but I don't
expect that that is what you want to do...  The papers which might interest
you are the EFT paper (this is very old now, but it explains the logic
of case expressions that I am using) and the "final technical report".
You might also look at the Watson documentation; its front end is an
incomplete draft of a paper on the prover as it now stands.

I originally used combinatory logic (a version equivalent to NFU), but
I switched over to lambda calculus (use of bound variables) because
combinatory logic is NOT user-friendly no matter how you slice it.

And God posted an angel with a flaming sword at | Sincerely, M. Randall Holmes
the gates of Cantor's paradise, that the       | Boise State U. (disavows all) 
slow-witted and the deliberately obtuse might | holmes at math.idbsu.edu
not glimpse the wonders therein. | http://math.idbsu.edu/~holmes