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$)反驳的树状规模与空间特征。具体而言，我们引入一类可扩展公式，并利用证明者-延迟者博弈证明其树状规模下界以及空间下界。此类公式具有特殊意义，因其包含许多经典组合原理，包括鸽巢原理、序原理及稠密线性序原理。此外，我们提出了Res($\oplus$)的宽度-空间关系，推广了Atserias与Dalmau（J. Comput. Syst. Sci.'08）的结果及其对应的破坏者-复制者博弈变体。