We consider the proof system Res 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 .We study characterizations of tree-like size and space of Res 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 generalizing the results by Atserias and Dalmau (J. Comput. Syst. Sci.'08) and their variant of Spoiler-Duplicator games. © 2024 Copyright held by the owner/author(s). Publication rights licensed to ACM.
Original languageEnglish
Number of pages15
JournalACM Transactions on Computation Theory
Volume16
Issue number3
DOIs
StatePublished - 30 Sep 2024

    Research areas

  • combinatorial games, linear resolution, lower bounds, Resolution, space complexity, Theorem proving, Combinatorial game, Linear Ordering principle, Linear resolutions, Low bound, Proof system, Prover-Delayer games, Resolution proofs, Space complexity, Trees (mathematics)

ID: 126386676