loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2008 23rd Annual IEEE Symposium on Logic in Computer Science
On the Asymptotic Nullstellensatz and Polynomial Calculus Proof Complexity
June 24-June 27
ISBN: 978-0-7695-3183-0
We show that the asymptotic complexity of uniformly generated (expressible in First-Order (FO) logic) propositional 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) \in \Omega(\log(n)) for NS and l(n) \in \Omega(\log(\log(n)) for PC, such that the propositional 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 inifinite 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) \in n^\Omega(1) or even for l(n) \in \Omega(n).??Finally, we show that for any non-empty proper subset A \subseteq \(i), (ii), (iii), (iv)\ the decision problem of whether a given input FO formula \psi has type belonging to A -??is undecidable.
Index Terms:
Propositional proof complexity, predicate logic, Algebraic proof complexity
Citation:
S? Riis, "On the Asymptotic Nullstellensatz and Polynomial Calculus Proof Complexity," lics, pp.272-283, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, 2008
Usage of this product signifies your acceptance of the Terms of Use.