Lower Bounds on Tree-like Size and Space of Resolution Proofs over Linear Equations
The paper studies characterizations of tree-like size and space of resolution proofs over linear equations (Res(⊕)) using combinatorial games. It introduces a class of extensible formulas and proves lower bounds on their tree-like size and space complexity.