On optimal proof systems and logics for PTIME.

Electronic Colloquium on Computational Complexity (ECCC)（2010）

引用 14|浏览306

暂无评分

摘要

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.

查看译文

关键词

p-optimal proof system,log h,fixed-point logic,function h,effective p-optimal proof system,polynomial time,finite structure,time constructible,fixed point

AI 理解论文

溯源树

样例

生成溯源树，研究论文发展脉络

Chat Paper

正在生成论文摘要