Open AccessA Complexity Gap for Tree-Resolution
Author(s) -
Søren Riis
Publication year - 1999
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v6i29.20098
Subject(s) - mathematical proof , mathematics , undecidable problem , proof complexity , discrete mathematics , decidability , resolution (logic) , tree (set theory) , combinatorics , sequence (biology) , computer science , biology , genetics , geometry , artificial intelligence
It is shown that any sequence psi_n of tautologies which expresses the validity of a fixed combinatorial principle either is "easy" i.e. has polynomial size tree-resolution proofs or is "difficult" i.e requires exponential size tree-resolution proofs. It is shown that the class of tautologies which are hard (for tree-resolution) is identical to the class of tautologies which are based on combinatorial principles which are violated for infinite sets. Actually it is shown that the gap-phenomena is valid for tautologies based on infinite mathematical theories (i.e. not just based on a single proposition). We clarify the link between translating combinatorial principles (or more general statements from predicate logic) and the recent idea of using the symmetrical group to generate problems of propositional logic. Finally, we show that it is undecidable whether a sequence psi_n (of the kind we consider) has polynomial size tree-resolution proofs or requires exponential size tree-resolution proofs. Also we show that the degree of the polynomial in the polynomial size (in case it exists) is non-recursive, but semi-decidable. Keywords: Logical aspects of Complexity, Propositional proof complexity, Resolution proofs.