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.