The proof system Res(PC_1/R) is a natural extension of the Resolution proof system that instead of clauses of literals operates with disjunctions of degree d polynomials over a ring R with boolean variables. Proving super-polynomial lower bounds for the size of Res(PC_1/R)-refutations of CNFs is one of the important problems in propositional proof complexity. The existence of such lower bounds is even open for Res(PC_1/\mathbb{F}) when \mathbb{F} is a finite field such as \mathbb{F}_2. In this paper, we investigate Res(PC_1/R) and tree-like Res(PC_1/R) and prove size-width relations for them when R is a finite ring. As an application, we get for every finite field \mathbb{F} the following lower bounds on the number of clauses:

(1) We prove almost quadratic lower bounds for Res(PC_d/\mathbb{F})-refutations for every fixed d. The new lower bounds are for the following CNFs:

(a) mod q Tseitin formulas (char(\mathbb{F})\neq q),

(b) Random k-CNFs with linearly many clauses.

(2) We also prove super-polynomial and exponential lower bounds for tree-like Res(PC_d/\mathbb{F})-refutations where d is not too large with respect to n for the following CNFs:

(a) mod q Tseitin formulas (char(\mathbb{F})\neq q),
(b) Random k-CNFs,
(c) Pigeonhole principle.

The above results imply the first nontrivial lower bounds for Res(\oplus) [Itsykson and Sokolov '14, Itsykson and Sokolov '20], Res(lin_\mathbb{F}) where \mathbb{F} is a finite field [Part and Tzameret '20], and R(PC_d/\mathbb{F}_2) [Kraj{\'\i}{\v{c}}ek '18]. Moreover, they imply the first super-polynomial and exponential lower bounds for tree-like R(PC_d/\mathbb{F}_2)-refutations of mod q Tseitin formulas, random k-CNFs, and the Pigeonhole principle.

New lower bounds for PHP^m_n were added.

The proof system Res(PC_d/R) is a natural extension of the Resolution proof system that instead of clauses of literals operates with disjunctions of degree d polynomials over a ring R with boolean variables. Proving super-polynomial lower bounds for the size of Res(PC_1/R)-refutations of CNFs is one of the important problems in propositional proof complexity. The existence of such lower bounds is even open for Res(PC_1/\mathbb{F}) when \mathbb{F} is a finite field such as \mathbb{F}_2. In this paper, we investigate Res(PC_d/R) and tree-like Res(PC_d/R) and prove size-width relations for them when R is a finite ring. As an application, we get for every finite field \mathbb{F} the following lower bounds on the number of clauses:
(1) We prove almost quadratic lower bounds for Res(PC_d/\mathbb{F})-refutations for every fixed d. The new lower bounds are for the following CNFs:
(a) mod q Tseitin formulas (char(\mathbb{F})\neq q),
(b) Random k-CNFs with linearly many clauses.
(2) We also prove super-polynomial and exponential lower bounds for tree-like Res(PC_d/\mathbb{F})-refutations where d is not too large with respect to n for the following CNFs:
(a) mod q Tseitin formulas (char(\mathbb{F})\neq q),
(b) Random k-CNFs.
The above results imply the first nontrivial lower bounds for Res(\oplus) \cite{is,is2}, Res(lin_\mathbb{F}) where \mathbb{F} is a finite field \cite{pt}, and R(PC_d/\mathbb{F}_2) \cite{krrandom}. Moreover, they imply the first super-polynomial and exponential lower bounds for tree-like R(PC_d/\mathbb{F}_2)-refutations of mod q Tseitin formulas and random k-CNFs.

Added detailed proofs of the main theorems.

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 bounds for CNFs with current methods. The reachable goal might be proving lower bounds for {Res}_R({lin}) when R is a finite field such as \mathbb{F}_2. Interestingly, {Res}_{\mathbb{F}_2}({lin}) is also fairly strong, and there is no known nontrivial lower bound for it, but for {Res}^*_R({lin}) (tree-like {Res}_R({lin})) we know exponential lower bounds for every finite field.
For the stronger systems {Res}_R({PC}_d) and {Res}_R^*({PC}_d) for d>1 on finite ring R, there is no known lower bounds till now. In this paper we will investigate these refutation systems and make some progress toward understanding these systems, including the case d=1. We prove a size-width relation for {Res}_R({PC}_d) and {Res}^*_R({PC}_d) for every finite ring R. This relation is proved by a new idea to reduce the problem to the original Ben-Sasson and Wigderson size-width relation for {Res} and {Res}^* using extension variables. As a by product, we get the following new lower bounds for every finite field \mathbb{F}:
(1) We prove the first nontrivial lower bounds for {Res}_\mathbb{F}({PC}_d) for fixed d: a nearly quadratic lower bounds for:
(a) mod q Tseitin formulas (char(\F)\neq q),
(b) Random k-CNFs with linearly many clauses.
(2) We also prove superpolynomial and exponential lower bounds for {Res}^*_\mathbb{F}({PC}_{d}) where d is not too large with respect to n for the following principles:
(a) mod q Tseitin formulas (char(\mathbb{F})\neq q),
(b) Random k-CNFs.

Fixed some typos
Add a new corollary about random cnfs

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 bounds for CNFs with current methods. The reachable goal might be proving lower bounds for {Res}_R({lin}) when R is a finite field such as \mathbb{F}_2. Interestingly, {Res}_{\mathbb{F}_2}({lin}) is also fairly strong, and there is no known nontrivial lower bound for it, but for {Res}^*_R({lin}) (tree-like {Res}_R({lin})) we know exponential lower bounds for every finite field.
For the stronger systems {Res}_R({PC}_d) and {Res}_R^*({PC}_d) for d>1 on finite ring R, there is no known lower bounds till now. In this paper we will investigate these refutation systems and make some progress toward understanding these systems, including the case d=1. We prove a size-width relation for {Res}_R({PC}_d) and {Res}^*_R({PC}_d) for every finite ring R. This relation is proved by a new idea to reduce the problem to the original Ben-Sasson and Wigderson size-width relation for {Res} and {Res}^* using extension variables. As a by product, we get the following new lower bounds for every finite field \mathbb{F}:
(1) We prove the first nontrivial lower bounds for {Res}_\mathbb{F}({PC}_d) for fixed d: a nearly quadratic lower bounds for mod q Tseitin formulas (char(\mathbb{F})\neq q) for suitable graphs.
(2) We also prove superpolynomial and exponential lower bounds for {Res}^*_\mathbb{F}({PC}_{d}) where d is not too large with respect to n for the following principles:
(a) mod q Tseitin formulas (char(\mathbb{F})\neq q),
(b) Random k-CNFs.