Riis, Søren A complexity gap for tree resolution. (English) Zbl 0994.03005 Comput. Complexity 10, No. 3, 179-209 (2001). Summary: This paper shows 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. Further it is shown that the gap phenomenon is valid for tautologies based on infinite mathematical theories (i.e. not just based on a single proposition).A corollary to this classification is that it is undecidable whether a sequence \(\psi_n\) has polynomial size tree-resolution proofs or requires exponential size tree-resolution proofs. It also follows that the degree of the polynomial in the polynomial size (in case it exists) is non-recursive, but semi-decidable. Cited in 15 Documents MSC: 03B35 Mechanization of proofs and logical operations 03F20 Complexity of proofs 03B05 Classical propositional logic 03C13 Model theory of finite structures 03B25 Decidability of theories and sets of sentences 68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) Keywords:satisfiability; tree-resolution proofs; combinatorial principles; gap phenomenon; infinite mathematical theories; hard propositional tautologies; propositional proof complexity PDFBibTeX XMLCite \textit{S. Riis}, Comput. Complexity 10, No. 3, 179--209 (2002; Zbl 0994.03005) Full Text: DOI