Some subsystems of constant-depth Frege with parity
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F18%3A00500314" target="_blank" >RIV/67985840:_____/18:00500314 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1145/3243126" target="_blank" >http://dx.doi.org/10.1145/3243126</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1145/3243126" target="_blank" >10.1145/3243126</a>
Alternative languages
Result language
angličtina
Original language name
Some subsystems of constant-depth Frege with parity
Original language description
We consider three relatively strong families of subsystems of AC0[2]-Frege proof systems, i.e., propositional proof systems using constant-depth formulas with an additional parity connective, for which exponential lower bounds on proof size are known. In order of increasing strength, the subsystems are (i) constant-depth proof systems with parity axioms and the (ii) treelike and (iii) daglike versions of systems introduced by Krajíček which we call PKcd(⊕). In a PKcd(⊕)-proof, lines are disjunctions (cedents) in which all disjuncts have depth at most d, parities can only appear as the outermost connectives of disjuncts, and all but c disjuncts contain no parity connective at all.nWe prove that treelike PKO(1)O(1)(⊕) is quasipolynomially but not polynomially equivalent to constant-depth systems with parity axioms. We also verify that the technique for separating parity axioms from parity connectives due to Impagliazzo and Segerlind can be adapted to give a superpolynomial separation between daglike PKO(1)O(1)(⊕) and AC0[2]-Frege, the technique is inherently unable to prove superquasipolynomial separations.nWe also study proof systems related to the system Res-Lin introduced by Itsykson and Sokolov. We prove that an extension of treelike Res-Lin is polynomially simulated by a system related to daglike PKO(1)O(1)(⊕), and obtain an exponential lower bound for this system.
Czech name
—
Czech description
—
Classification
Type
J<sub>imp</sub> - Article in a specialist periodical, which is included in the Web of Science database
CEP classification
—
OECD FORD branch
10101 - Pure mathematics
Result continuities
Project
—
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2018
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
ACM Transactions on Computational Logic
ISSN
1529-3785
e-ISSN
—
Volume of the periodical
19
Issue of the periodical within the volume
4
Country of publishing house
US - UNITED STATES
Number of pages
34
Pages from-to
—
UT code for WoS article
000452804000006
EID of the result in the Scopus database
2-s2.0-85057166384