Standard

Resolution Over Linear Equations: Combinatorial Games for Tree-like Size and Space. / Gryaznov, S.; Ovcharov, S.; Riazanov, A.

In: ACM Transactions on Computation Theory, Vol. 16, No. 3, 30.09.2024.

Research output: Contribution to journal › Article › peer-review

Harvard

Gryaznov, S, Ovcharov, S & Riazanov, A 2024, 'Resolution Over Linear Equations: Combinatorial Games for Tree-like Size and Space', ACM Transactions on Computation Theory, vol. 16, no. 3. https://doi.org/10.1145/3675415

APA

Gryaznov, S., Ovcharov, S., & Riazanov, A. (2024). Resolution Over Linear Equations: Combinatorial Games for Tree-like Size and Space. ACM Transactions on Computation Theory, 16(3). https://doi.org/10.1145/3675415

Vancouver

Gryaznov S, Ovcharov S, Riazanov A. Resolution Over Linear Equations: Combinatorial Games for Tree-like Size and Space. ACM Transactions on Computation Theory. 2024 Sep 30;16(3). https://doi.org/10.1145/3675415

Author

Gryaznov, S. ; Ovcharov, S. ; Riazanov, A. / Resolution Over Linear Equations: Combinatorial Games for Tree-like Size and Space. In: ACM Transactions on Computation Theory. 2024 ; Vol. 16, No. 3.

BibTeX

@article{287d7ccbac4b4c4e962d8aec13064754,
title = "Resolution Over Linear Equations: Combinatorial Games for Tree-like Size and Space",
abstract = "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. {\textcopyright} 2024 Copyright held by the owner/author(s). Publication rights licensed to ACM.",
keywords = "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)",
author = "S. Gryaznov and S. Ovcharov and A. Riazanov",
note = "Export Date: 19 October 2024 Адрес для корреспонденции: Gryaznov, S.; Imperial College LondonUnited Kingdom; эл. почта: svyatoslav.i.gryaznov@gmail.com Сведения о финансировании: Russian Science Foundation, RSF, 18-71-10042 Сведения о финансировании: Russian Science Foundation, RSF Текст о финансировании 1: The research is supported by Russian Science Foundation (project 18-71-10042).",
year = "2024",
month = sep,
day = "30",
doi = "10.1145/3675415",
language = "Английский",
volume = "16",
journal = "ACM Transactions on Computation Theory",
issn = "1942-3454",
publisher = "Association for Computing Machinery",
number = "3",

}

RIS

TY - JOUR

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

AU - Gryaznov, S.

AU - Ovcharov, S.

AU - Riazanov, A.

N1 - Export Date: 19 October 2024 Адрес для корреспонденции: Gryaznov, S.; Imperial College LondonUnited Kingdom; эл. почта: svyatoslav.i.gryaznov@gmail.com Сведения о финансировании: Russian Science Foundation, RSF, 18-71-10042 Сведения о финансировании: Russian Science Foundation, RSF Текст о финансировании 1: The research is supported by Russian Science Foundation (project 18-71-10042).

PY - 2024/9/30

Y1 - 2024/9/30

N2 - 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.

AB - 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.

KW - combinatorial games

KW - linear resolution

KW - lower bounds

KW - Resolution

KW - space complexity

KW - Theorem proving

KW - Combinatorial game

KW - Linear Ordering principle

KW - Linear resolutions

KW - Low bound

KW - Proof system

KW - Prover-Delayer games

KW - Resolution proofs

KW - Space complexity

KW - Trees (mathematics)

UR - https://www.mendeley.com/catalogue/72447750-c20e-3812-a2e3-ef849478ff44/

U2 - 10.1145/3675415

DO - 10.1145/3675415

M3 - статья

VL - 16

JO - ACM Transactions on Computation Theory

JF - ACM Transactions on Computation Theory

SN - 1942-3454

IS - 3

ER -

ID: 126386676