Articles
The Mutilated Checkerboard in Set Theory
This paper was presented at the QED meeting in Warsaw in 1995 July. It is a proof in set theory that I think an interactive prover for heavy duty set theory should be able to accept. It uses for a different purpose the same problem as the previous paper.The Mutilated Checkerboard in Set Theory was presented at the QED meeting in Warsaw in 1995 July. It is a proof in set theory that I think an interactive prover for heavy duty set theory should be able to accept.
My 1964 memorandum A Tough Nut for Theorem Provers has attracted some interest lately, and there is something more about it at in the above URL.
Download the article in PDF.