Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR21-053 | 13th April 2021 10:06

Information in propositional proofs and algorithmic proof search


Authors: Jan Krajicek
Publication: 13th April 2021 10:34
Downloads: 403


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 w.r.t. all 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 {\bf 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$ 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 $\tau$ with short proofs but having large information measure $i_P(\tau)$.
We isolate and motivate the problem to establish {\em 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.

ISSN 1433-8092 | Imprint