ECCC-Report TR10-008https://eccc.weizmann.ac.il/report/2010/008Comments and Revisions published for TR10-008en-usThu, 08 Apr 2010 10:26:55 +0300
Revision 1
| On optimal proof systems and logics for PTIME |
Yijia Chen,
Joerg Flum
https://eccc.weizmann.ac.il/report/2010/008#revision1We 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 {\em effective} $p$-optimal proof system if $\textup{NTIME}(h^{O(1)}) \not\subseteq \textup{DTIME}(h^{O(\log h)})$ for every time constructible and increasing function $h$.Thu, 08 Apr 2010 10:26:55 +0300https://eccc.weizmann.ac.il/report/2010/008#revision1
Paper TR10-008
| On optimal proof systems and logics for PTIME |
Yijia Chen,
Joerg Flum
https://eccc.weizmann.ac.il/report/2010/008We prove that TAUT has a $p$-optimal proof system if and only if $L_\le$, a logic introduced in [Gurevich, 88], is a P-bounded logic for P. Furthermore, using the method developed in [Chen and Flum, 10], we show that TAUT has no \emph{effective} $p$-optimal proof system under some reasonable complexity-theoretic assumption.Fri, 15 Jan 2010 18:18:11 +0200https://eccc.weizmann.ac.il/report/2010/008