A complexity gap for tree resolution
A complexity gap for tree resolution
复制标题
树解析的复杂性差距
DOI：
--
复制
发表时间：
1999
影响因子：
1.4
通讯作者：
Søren Riis
中科院分区：
文献类型：
--
作者：
Søren Riis
抽象的。本文证明了任何序列
表示固定组合原理有效性的重言式的$psi_n$或者是“容易”的，即具有多项式大小的树分解证明，或者是“困难”的，即需要指数大小的树分解证明。证明了(对于树分解)困难的重言式类与基于无限集违反的组合原理的重言式类是相同的。此外，还证明了间隙现象对于基于无限数学理论的重言式是有效的(即，不仅仅是基于单个命题)。
$psi_n$具有多项式大小的树分解证明或需要指数大小的树分解证明。它还得出多项式在多项式大小中的次数(如果存在的话)是非递归的，但是半可判定的。
Abstract. 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.