Classification of the asymptotic Proof Complexity of Polynomial Calculus
View/ Open
Published version
Embargoed until: 5555-01-01
Reason: Version Not Permitted
Embargoed until: 5555-01-01
Reason: Version Not Permitted
Publisher
Journal
Graphs and Combinatorics
ISSN
0911-0119
Metadata
Show full item recordAbstract
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) ∈ Ω(log(n)) for NS and l(n) ∈
Ω(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