INFORMATION IN PROPOSITIONAL PROOFS AND ALGORITHMIC PROOF SEARCH

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F22%3A10452385" target="_blank" >RIV/00216208:11320/22:10452385 - isvavai.cz</a>

Výsledek na webu

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

DOI - Digital Object Identifier

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

Jazyk výsledku

angličtina

Název v původním jazyce

INFORMATION IN PROPOSITIONAL PROOFS AND ALGORITHMIC PROOF SEARCH

Popis výsledku v původním jazyce

We study from the proof complexity perspective the (informal) proof search problem (cf. [17, Sections 1.5 and 21.5]):Is there an optimal way to search for propositional proofs?We note that, as a consequence of Levin&apos;s universal search, for any fixed proof system there exists a time-optimal proof search algorithm. Using classical proof complexity results about reflection principles we prove that a time-optimal proof search algorithm exists without restricting proof systems iff a p-optimal proof system exists.To characterize precisely the time proof search algorithms need for individual formulas we introduce a new proof complexity measure based on algorithmic information concepts. In particular, to a proof system P we attach information-efficiency function i(P)(tau) assigning to a tautology a natural number, and we show that:i(P)(tau) characterizes time any P-proof search algorithm has to use on tau,for a fixed P there is such an information-optimal algorithm (informally: it finds proofs of minimal information content),a proof system is information-efficiency optimal (its information-efficiency function is minimal up to a multiplicative constant) iff it is p-optimal,for non-automatizable systems P there are formulas tau with short proofs but having large information measure i(P)(tau).We isolate and motivate the problem to establish unconditional super-logarithmic lower bounds for i(P)(tau) where no super-polynomial size lower bounds are known. We also point out connections of the new measure with some topics in proof complexity other than proof search.

Název v anglickém jazyce

INFORMATION IN PROPOSITIONAL PROOFS AND ALGORITHMIC PROOF SEARCH

Popis výsledku anglicky

We study from the proof complexity perspective the (informal) proof search problem (cf. [17, Sections 1.5 and 21.5]):Is there an optimal way to search for propositional proofs?We note that, as a consequence of Levin&apos;s universal search, for any fixed proof system there exists a time-optimal proof search algorithm. Using classical proof complexity results about reflection principles we prove that a time-optimal proof search algorithm exists without restricting proof systems iff a p-optimal proof system exists.To characterize precisely the time proof search algorithms need for individual formulas we introduce a new proof complexity measure based on algorithmic information concepts. In particular, to a proof system P we attach information-efficiency function i(P)(tau) assigning to a tautology a natural number, and we show that:i(P)(tau) characterizes time any P-proof search algorithm has to use on tau,for a fixed P there is such an information-optimal algorithm (informally: it finds proofs of minimal information content),a proof system is information-efficiency optimal (its information-efficiency function is minimal up to a multiplicative constant) iff it is p-optimal,for non-automatizable systems P there are formulas tau with short proofs but having large information measure i(P)(tau).We isolate and motivate the problem to establish unconditional super-logarithmic lower bounds for i(P)(tau) where no super-polynomial size lower bounds are known. We also point out connections of the new measure with some topics in proof complexity other than proof search.

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í

2022

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

Journal of Symbolic Logic

ISSN

0022-4812

e-ISSN

—

Svazek periodika

2022

Číslo periodika v rámci svazku

87

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

18

Strana od-do

852-869

Kód UT WoS článku

000792183800001

EID výsledku v databázi Scopus

2-s2.0-85117311692