A Tough Nut for Tree Resolution
Stefan Dantchev
May 2000 |

## Abstract:
One of the earliest proposed hard problems for theorem provers
is a propositional version of the
Mutilated Chessboard problem.
It is well known from recreational mathematics: Given a chessboard having two
diagonally opposite squares removed, prove that it cannot be covered with
dominoes. In Proof Complexity, we consider not ordinary, but
mutilated chessboard. In the paper, we show a
lower bound for tree resolution.
Available as |

Last modified: 2003-06-08 by webmaster.