期刊名称:Electronic Colloquium on Computational Complexity
印刷版ISSN:1433-8092
出版年度:2010
卷号:2010
出版社:Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要: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 {\em effective} p-optimal proof system if \textupNTIME(hO(1))\textupDTIME(hO(logh)) for every time constructible and increasing function h.