In this talk, we will go over lower bounds for roABP-IPS refutations of Boolean CNF formulas. Earlier IPS lower bounds were mostly known for algebraic systems of equations, rather than CNF formulas, which are the standard objects in propositional proof complexity. We will discuss how the paper obtains such lower bounds using a feasible interpolation argument, where short roABP-IPS refutations would imply small monotone span programs for the corresponding interpolants. Therefore, lower bounds for monotone span programs can be used to give lower bounds for roABP-IPS refutations.
