TY - JOUR
AU - Stefan Dantchev
AU - SÃ¸ren Riis
PY - 2000/01/10
Y2 - 2020/08/12
TI - A Tough Nut for Tree Resolution
JF - BRICS Report Series
JA - BRICS
VL - 7
IS - 10
SE - Articles
DO - 10.7146/brics.v7i10.20137
UR - https://tidsskrift.dk/brics/article/view/20137
AB - One of the earliest proposed hard problems for theorem provers isa propositional version of the Mutilated Chessboard problem. It is wellknown from recreational mathematics: Given a chessboard having twodiagonally opposite squares removed, prove that it cannot be covered withdominoes. In Proof Complexity, we consider not ordinary, but 2n * 2nmutilated chessboard. In the paper, we show a 2^Omega(n) lower bound for tree resolution.
ER -