Delivery-Date: 
From: Geoff Sutcliffe <geoff@cs.jcu.edu.au>
Message-Id: <199508110433.OAA00457@coral.cs.jcu.edu.au>
Subject: Re: about the proof of the CheckerBoard Problem
To: lusk@mcs.anl.gov (Rusty Lusk)
Date: Fri, 11 Aug 1995 14:33:23 +1000 (+1000)
Cc: qed@antares.mcs.anl.gov
In-Reply-To: <199508101901.OAA27094@antares.mcs.anl.gov> from "Rusty Lusk" at Aug 10, 95 02:01:15 pm
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Length: 912
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

Hi,
 
> 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. 

If anyone would like to see and use Stickel's representation, it appears
as problems PUZ015-2 and PUZ016-2 of the forthcoming release of the
TPTP problem library. The release will be v1.2.0, and will be out soon.
The TPTP problem library can be accessed through the URLs:
      http://www.cs.jcu.edu.au/ftp/users/GSutcliffe/TPTP.HTML
      http://wwwjessen.informatik.tu-muenchen.de/~suttner/tptp.html

Cheers,

Geoff

Geoff Sutcliffe
Department of Computer Science    Email : geoff@cs.jcu.edu.au
James Cook University             Phone : +61 77 815085/814622
Townsville, Australia, 4811.      FAX   : +61 77 814029