Open AccessA Tough Nut for Tree Resolution
Author(s) -
Stefan Dantchev,
Søren Riis
Publication year - 2000
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v7i10.20137
Subject(s) - mathematics , resolution (logic) , combinatorics , omega , tree (set theory) , diagonal , upper and lower bounds , discrete mathematics , arithmetic , computer science , geometry , philosophy , linguistics , programming language , mathematical analysis
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 2n * 2n mutilated chessboard. In the paper, we show a 2^Omega(n) lower bound for tree resolution.