TY - JOUR AU - Dantchev, Stefan AU - Riis, Søren PY - 2000/01/10 Y2 - 2024/03/29 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 SP - AB - One of the earliest proposed hard problems for theorem provers is<br />a propositional version of the Mutilated Chessboard problem. It is well<br />known from recreational mathematics: Given a chessboard having two<br />diagonally opposite squares removed, prove that it cannot be covered with<br />dominoes. In Proof Complexity, we consider not ordinary, but 2n * 2n<br />mutilated chessboard. In the paper, we show a 2^Omega(n) lower bound for tree resolution. ER -