In Hrubeš' Algebraic Monotone Calculus AMC a DNF tautology $A$ is proved by a monotone arithmetic circuit computing $\chi(A)-\epsilon\cdot\chi(1)$ for some $\epsilon>0$, where $\chi(A)$ is the set-multilinear polynomial whose coefficient at $\mathbf x^{\sigma}$ counts the terms of $A$ satisfied by $\sigma$, and $\chi(1)=\prod_{i\le n}(x_i^0+x_i^1)$. Proof size is circuit size, and ... more >>>

Resolution over linear equations (introduced in [RT08]) emerged recently as an important object of study. This refutation system, denoted Res(lin$_R$), operates with disjunction of linear equations over a ring $R$. On the one hand, the system captures a natural ``minimal'' extension of resolution in which efficient counting can be achieved; ... more >>>