A map g:\{0,1\}^n\to\{0,1\}^m (m>n) is a hard proof complexity generator for a proof system P iff for every string b\in\{0,1\}^m\setminus Rng(g), formula \tau_b(g) naturally expressing b\not\in Rng(g) requires superpolynomial size P-proofs. One of the well-studied maps in the theory of proof complexity generators is Nisan--Wigderson generator. Razborov (Annals of Mathematics ... more >>>

The refutation system {Res}_R({PC}_d) is a natural extension of resolution refutation system such that it operates with disjunctions of degree d polynomials over ring R with boolean variables. For d=1, this system is called {Res}_R({lin}). Based on properties of R, {Res}_R({lin}) systems can be too strong to prove lower ... more >>>