On the Asymptotic Nullstellensatz and Polynomial Calculus Proof Complexity
On the Asymptotic Nullstellensatz and Polynomial Calculus Proof Complexity
复制标题
论渐近零值和多项式微积分证明复杂度
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Søren Riis
中科院分区：
文献类型：
--
作者：
Søren Riis
我们证明了一致生成的命题重言式的渐近复杂性（可在一阶（FO）逻辑中表达）的零星证明系统（NS）以及多项式演算（PC）在有限特征域上有四种不同类型的渐近行为。更确切地说，基于Krajicek的一些非常重要的工作，我们证明了对于每个素数p，存在函数l（n）G isin Ω（log（n）），对于NS和l（n）G Ω（log（log（n））对于PC，使得任何FO公式的介词翻译（在所有有限模型中失败），在特征为p的域上具有度证明复杂性，以4种相互不同的方式表现：（i）度复杂度受常数约束。(ii)对于所有n的值，度复杂度至少为l（n）。(iii)度复杂度至少是l（n），除了在有限数量的无限大小的正则连续性中，其中度是常数。(iv)度复杂度以一种非常特殊的方式波动，其中度复杂度在无限数量的规则连续性上取不同的常数值，每个规则连续性具有无限大小。我们把它作为一个开放的问题，是否分类仍然有效，l[n]是在nOmega（1），甚至为I（n）是在Omega（n）。最后，我们证明了对于任意非空的真子集A sube {（i），（ii），（iii），（iv）}，给定的输入FO公式Psi是否有属于A -的类型的判定问题是不可判定的.
We show that the asymptotic complexity of uniformly generated (expressible in first-order (FO) logic) prepositional tautologies for the nullstellensatz proof system (NS) as well as for polynomial calculus, (PC) has four distinct types of asymptotic behavior over fields of finite characteristic. More precisely, based on some highly non-trivial work by Krajicek, we show that for each prime p there exists a function l(n) G isin Omega(log(n)) for NS and l(n) G Omega (log(log(n)) for PC, such that the prepositional translation of any FO formula (that fails in all finite models), has degree proof complexity over fields of characteristic p, that behave in 4 mutually distinct ways: (i) The degree complexity is bound by a constant. (ii) The degree complexity is at least l(n) for all values of n. (iii) The degree complexity is at least l(n) except in a finite number of regular subsequences of infinite size, where the degree is constant. (iv) The degree complexity fluctuates in a very particular way with the degree complexity taking different constant values on an infinite number of regular subsequences each of infinite size. We leave it as an open question whether the classification remains valid for l[n) isin nOmega(1) or even for I (n) isin Omega(n). Finally, we show that for any non-empty proper subset A sube {(i), (ii), (iii), (iv)} the decision problem of whether a given input FO formula Psi has type belonging to A - is undecidable.
Lovász-Schrijver 和 Sherali-Adams 证明系统的等级复杂度差距
影响因子：
1.4
作者：
Dantchev S
通讯作者：
Dantchev S
参数化证明复杂性
影响因子：
1.4
作者：
Dantchev S
通讯作者：
Dantchev S