Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
	id OAA27120 for qed-out; Thu, 10 Aug 1995 14:01:31 -0500
Received: from mcs.anl.gov (donner.mcs.anl.gov [140.221.5.134]) by antares.mcs.anl.gov (8.6.10/8.6.10)  with ESMTP
	id OAA27094 for <qed>; Thu, 10 Aug 1995 14:01:16 -0500
Message-Id: <199508101901.OAA27094@antares.mcs.anl.gov>
To: qed
Subject: [Richard Waldinger: Re: about the proof of the CheckerBoard Problem]
Date: Thu, 10 Aug 1995 14:01:15 -0500
From: Rusty Lusk <lusk@mcs.anl.gov>
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


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)