A Tough Nut for Tree Resolution | Zendy

Stefan Dantchev | Zendy; Søren Riis | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A 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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research