Wolfgang Windsteiger,
"On a Solution of the mutilated Checkerboard Problem Using the Theorema Set Theory Prover"
: Proceedings of the 9th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, 6-2001
Original Titel:
On a Solution of the mutilated Checkerboard Problem Using the Theorema Set Theory Prover
Sprache des Titels:
Englisch
Original Buchtitel:
Proceedings of the 9th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning
Original Kurzfassung:
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 particular also
for automated set theory provers. In this paper, we are going to present a
complete proof of the checkerboard problem using the {\itshape Theorema}
{\itshape Set Theory prover}.
Forschungs-