INFORMATION IN PROPOSITIONAL PROOFS AND ALGORITHMIC PROOF SEARCH
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
INFORMATION IN PROPOSITIONAL PROOFS AND ALGORITHMIC PROOF SEARCH
Original language description
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'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.
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
2022
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
Journal of Symbolic Logic
ISSN
0022-4812
e-ISSN
—
Volume of the periodical
2022
Issue of the periodical within the volume
87
Country of publishing house
US - UNITED STATES
Number of pages
18
Pages from-to
852-869
UT code for WoS article
000792183800001
EID of the result in the Scopus database
2-s2.0-85117311692