文章基本信息

标题：Information in propositional proofs and algorithmic proof search
本地全文：下载
作者：Jan Krajicek
期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：2021
卷号：21
语种：English
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：We study from the proof complexity perspective the (informal) proof search problem (cf. [16, Secs.1.5 and 21.5]): • 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 information-efficiency function iP (τ ) assigning to a tautology a natural number, and we show that: • iP (τ ) characterizes time any P-proof search algorithm has to use on τ 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 τ with short proofs but having large information measure iP (τ ). We isolate and motivate the problem to establish unconditional super logarithmic lower bounds for iP (τ ) 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.