Information in propositional proofs and algorithmic proof search

DOI10.1017/JSL.2021.75MaRDI QIDQ6364953arXivWikidataFDO

Authors Jan Krajíček

Publication date 10 April 2021

Published in arXiv

Full work available at URL https://doi.org/10.1017/JSL.2021.75

Mathematics Subject Classification ID

Complexity of proofs (03F20) Communication complexity, information complexity (68Q11) Algorithmic information theory (Kolmogorov complexity, etc.) (68Q30)

arXiv classification

cs.CCmath.LO

Abstract: We study from the proof complexity perspective the (informal) proof search problem: Is there an optimal way to search for propositional proofs? We note that 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 {�f information-efficiency function} $i_P(au)$ assigning to a tautology a natural number, and we show that: - $i_P(au)$ characterizes time any $P$-proof search algorithm has to use on $au$ and that for a fixed $P$ there is such an information-optimal algorithm, - a proof system is information-efficiency optimal iff it is p-optimal, - for non-automatizable systems $P$ there are formulas $au$ with short proofs but having large information measure $i_P(au)$. We isolate and motivate the problem to establish unconditional super-logarithmic lower bounds for $i_P(au)$ 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.

This page was built for publication: Information in propositional proofs and algorithmic proof search

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6364953)