期刊名称：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.
