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

• Type: Journal
• Year: 2010
• Where: ECCC
• Authors: Yijia Chen, Jörg Flum
• Keywords: ECCC 2010, Effective P-optimal Proof, Fixed-point Logic, P-optimal Proof