Resolution Over Linear Equations: Combinatorial Games for Tree-like Size and Space

Svyatoslav Gryaznov, Sergei Ovcharov, Artur Riazanov

We consider the proof system Res($\oplus$) introduced by Itsykson and Sokolov (Ann. Pure Appl. Log.'20), which is an extension of the resolution proof system and operates with disj…