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 disjunctions of linear equations over $\mathbb{F}_2$. We study characterizations of tree-like size and space of Res($\oplus$) refutations using combinatorial games. Namely, we introduce a class of extensible formulas and prove tree-like size lower bounds on it using Prover-Delayer games, as well as space lower bounds. This class is of particular interest since it contains many classical combinatorial principles, including the pigeonhole, ordering, and dense linear ordering principles. Furthermore, we present the width-space relation for Res($\oplus$) generalizing the results by Atserias and Dalmau (J. Comput. Syst. Sci.'08) and their variant of Spoiler-Duplicator games.

翻译：我们考虑由Itsykson和Sokolov（Ann. Pure Appl. Log.'20）引入的证明系统Res($\oplus$)，它是消解证明系统的扩展，处理的是$\mathbb{F}_2$上线性方程析取式。我们利用组合博弈研究Res($\oplus$)反驳的树状规模和空间的刻画。具体而言，我们引入一类可扩展公式，并通过Prover-Delayer博弈证明其树状规模下界以及空间下界。这类公式特别值得关注，因为它包含许多经典组合原理，包括鸽巢原理、序原理和稠密线性序原理。此外，我们给出Res($\oplus$)的宽度-空间关系，推广了Atserias和Dalmau（J. Comput. Syst. Sci.'08）的结果及其Spoiler-Duplicator博弈的变体。