Return-Path: Delivery-Date: Received: from antares.mcs.anl.gov (actually mcs.anl.gov !OR! owner-qed@mcs.anl.gov) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 10 Aug 1995 20:05:59 +0100 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 ; Thu, 10 Aug 1995 14:01:16 -0500 Message-Id: <199508101901.OAA27094@antares.mcs.anl.gov> To: qed@antares.mcs.anl.gov Subject: [Richard Waldinger: Re: about the proof of the CheckerBoard Problem] Date: Thu, 10 Aug 1995 14:01:15 -0500 From: Rusty Lusk 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)