=ADD=
=reftype=
14
=number=
01-26
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/2001/01-26.ps.gz
=year=
2001
=month=
12
=author=
Windsteiger; Wolfgang
=title=
On a Solution of the Mutilated Checkerboard Problem using the Theorema Set Theory Prover
=abstract=
The Mutilated Checkerboard Problem has some tradition as a benchmark problem
  for automated theorem proving systems. Informally speaking, it states that
  an 8 by 8 checkerboard with the two opposite corners removed cannot be
  covered by dominoes. Various solutions using different approaches have been
  presented since its original statement by John McCarthy in 1964. An elegant
  four-line proof has been given on paper by McCarthy himself in 1995, which
  is based on a formulation of the original problem in set theory. Since
then,  the checkerboard problem stands as a benchmark problem in particularalso
  for automated set theory provers. In this paper, we are going to present a
  complete proof of the checkerboard problem using the \emph{Theorema
  Set Theory prover}.
=note=
submitted to Special Issue of JSC, also available as SFB report 01-24
=sponsor=
SFB Numerical and Symbolic Scientific Computing (F013) at the University of Linz, the ``PROVE Project'' supported by the regional government of Upper Austria, and the european union ``CALCULEMUS Project'' (HPRN--CT--2000--00102).
=keywords=
Theorema, Automated Theorem Proving, Checkerboard