ON THE EXISTENCE OF STRONG PROOF COMPLEXITY GENERATORS

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F24%3A10487986" target="_blank" >RIV/00216208:11320/24:10487986 - isvavai.cz</a>

Výsledek na webu

<a href="https://verso.is.cuni.cz/pub/verso.fpl?fname=obd_publikace_handle&handle=Y.rqPZkIUZ" target="_blank" >https://verso.is.cuni.cz/pub/verso.fpl?fname=obd_publikace_handle&handle=Y.rqPZkIUZ</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1017/bsl.2023.40" target="_blank" >10.1017/bsl.2023.40</a>

Jazyk výsledku

angličtina

Název v původním jazyce

ON THE EXISTENCE OF STRONG PROOF COMPLEXITY GENERATORS

Popis výsledku v původním jazyce

Cook and Reckhow [5] pointed out that $mathcal {N}mathcal {P} neq comathcal {N}mathcal {P}$ iff there is no propositional proof system that admits polynomial size proofs of all tautologies. The theory of proof complexity generators aims at constructing sets of tautologies hard for strong and possibly for all proof systems. We focus on a conjecture from [16] in foundations of the theory that there is a proof complexity generator hard for all proof systems. This can be equivalently formulated (for p-time generators) without a reference to proof complexity notions as follows:There exists a p-time function g stretching each input by one bit such that its range $rng(g)$ intersects all infinite $mathcal {N}mathcal {P}$ sets. We consider several facets of this conjecture, including its links to bounded arithmetic (witnessing and independence results), to time-bounded Kolmogorov complexity, to feasible disjunction property of propositional proof systems and to complexity of proof search. We argue that a specific gadget generator from [18] is a good candidate for g. We define a new hardness property of generators, the $bigvee $ -hardness, and show that one specific gadget generator is the $bigvee $ -hardest (w.r.t. any sufficiently strong proof system). We define the class of feasibly infinite $mathcal {N}mathcal {P}$ sets and show, assuming a hypothesis from circuit complexity, that the conjecture holds for all feasibly infinite $mathcal {N}mathcal {P}$ sets.

Název v anglickém jazyce

ON THE EXISTENCE OF STRONG PROOF COMPLEXITY GENERATORS

Popis výsledku anglicky

Cook and Reckhow [5] pointed out that $mathcal {N}mathcal {P} neq comathcal {N}mathcal {P}$ iff there is no propositional proof system that admits polynomial size proofs of all tautologies. The theory of proof complexity generators aims at constructing sets of tautologies hard for strong and possibly for all proof systems. We focus on a conjecture from [16] in foundations of the theory that there is a proof complexity generator hard for all proof systems. This can be equivalently formulated (for p-time generators) without a reference to proof complexity notions as follows:There exists a p-time function g stretching each input by one bit such that its range $rng(g)$ intersects all infinite $mathcal {N}mathcal {P}$ sets. We consider several facets of this conjecture, including its links to bounded arithmetic (witnessing and independence results), to time-bounded Kolmogorov complexity, to feasible disjunction property of propositional proof systems and to complexity of proof search. We argue that a specific gadget generator from [18] is a good candidate for g. We define a new hardness property of generators, the $bigvee $ -hardness, and show that one specific gadget generator is the $bigvee $ -hardest (w.r.t. any sufficiently strong proof system). We define the class of feasibly infinite $mathcal {N}mathcal {P}$ sets and show, assuming a hypothesis from circuit complexity, that the conjecture holds for all feasibly infinite $mathcal {N}mathcal {P}$ sets.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10101 - Pure mathematics

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2024

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Bulletin of Symbolic Logic

ISSN

1079-8986

e-ISSN

1943-5894

Svazek periodika

30

Číslo periodika v rámci svazku

1

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

21

Strana od-do

20-40

Kód UT WoS článku

001195451000001

EID výsledku v databázi Scopus

2-s2.0-85178007044