Re: practical Proof Checking systems
John McCarthy (jmc@Steam.Stanford.EDU)
Mon, 18 Mar 1996 14:26:14 -0800 (PST)
I would be grateful if someone would try the 4 step proof of the
mutilated checkerboard theorem in HOL and see how close they can come
to the 4 steps.
The problem and the informal proof were presented at the Warsaw
meeting and are also on my home page
http://www-formal.stanford.edu/jmc/.