On p-Optimal Proof Systems and Logics for PTIME

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 effectively p-optimal proof system if NTIME(hO(1) ) ⊆ DTIME(hO(log h) ) for every time constructible and increasing function h.

• Type: Conference
• Year: 2010
• Where: ICALP
• Authors: Yijia Chen, Jörg Flum
• Keywords: Captures Polynomial Time, ICALP 2010, Increasing Function H, P-optimal Proof, Programming Languages