文章基本信息

标题：Optimal proof systems for Propositional Logic and complete sets
本地全文：下载
作者：Jochen Me\3ner, Jacobo Toran
期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：1997
卷号：1997
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：A polynomial time computable function h: whose range is the set of tautologies in Propositional Logic (TAUT), is called a proof system. Cook and Reckhow defined this concept and in order to compare the relative strenth of different proof systems, they considered the notion of p-simulation. Intuitively a proof system h p-simulates a second one h if there is a polynomial time computable function translating proofs in h into proofs in h. A proof system is called optimal if it p-simulates every other proof system. The question of whether p-optimal proof systems exist is an important one in the field. Kraj\'{\i}\v{c}ek and Pudl\'ak have given a sufficient condition for the existence of such optimal systems, showing that if the deterministic and nondeterministic exponential time classes coincide, then p-optimal proof systems exist. They also give a condition implying the existence of optimal proof systems (a related concept to the one of p-optimal systems) exist. In this paper we improve this result giving a weaker sufficient condition for this fact. We show that if a particular class of sets with low information content in nondeterministic double exponential time is included in the corresponding nondeterministic class, then p-optimal proof systems exist. We also show some complexity theoretical consequences that follow from the assumption of the existence of p-optimal systems. We prove that if p-optimal systems exist the the class UP (an some other related complexity classes) have many-one complete languages, and that many-one complete sets for NP SPARSE follow from the existence of optimal proof systems.
关键词：complete sets, propositional proof systems