On optimal proof systems and logics for PTIME.
Yijia Chen, Jörg Flum · 2010
We prove that TAUT has a p-optimal proof system if and only if a logic related to least fixed-point logic captures polynomial time on all finite structures. Furthermore, we show that TAUT has no effec-tive p-optimal proof system if NTIME(hO(1)) 6 ⊆ DTIME(hO(log h)) for every time constructible and increasing function h. 1.