[Richard Waldinger: Re: about the proof of the CheckerBoard Problem]
Rusty Lusk (lusk@mcs.anl.gov)
Thu, 10 Aug 1995 14:01:15 -0500
mark stickel used a prpositional logic representation to prove the theorem
for 8x8 and some larger boards without using the color representation, just
using exhaustive search (a fast implementation of davis-putnam). the work is
reported in the recent paper of stickel and uribe. of course this bypasses
the point of mccarthy's challenge and doesnt establish the general case.
there is a recent paper by a student of boyer using the boyer moore theorem
prover to get the general result. the proof is interactive and uses the
coloring argument. it is the subject of a paper that has been submitted to a
recent journal, perhaps journal of symbolic systems (?).
maybe these were mentioned at QED2, i wasn't there---richard
(Actually from Richard, only posted by me - Rusty)