| Identifikační kód |
RIV/67985840:_____/18:00500314 |
| Název v anglickém jazyce |
Some subsystems of constant-depth Frege with parity |
| Druh |
J - Recenzovaný odborný článek (Jimp, Jsc a Jost) |
| Poddruh |
J/A - Článek v odborném periodiku je obsažen v databázi Web of Science společností Thomson Reuters s příznakem „Article“, „Review“ nebo „Letter“ (Jimp) |
| Jazyk |
eng - angličtina |
| Vědní obor |
10101 - Pure mathematics |
| Rok uplatnění |
2018 |
| Kód důvěrnosti údajů |
S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
| Počet výskytů výsledku |
1 |
| Počet tvůrců celkem |
2 |
| Počet domácích tvůrců |
1 |
| Výčet všech uvedených jednotlivých tvůrců |
Michal Garlík (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 9192255)
L. A. Kołodziejcz (státní příslušnost: PL - Polská republika) |
| Popis výsledku v anglickém jazyce |
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. |
| Klíčová slova oddělená středníkem |
constant-depth Frege;counting axioms;modular counting;propositional proof complexity |
| Stránka www, na které se nachází výsledek |
- |
| DOI výsledku |
10.1145/3243126 |
| Odkaz na údaje z výzkumu |
- |