Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR97-026 | 18th June 1997 00:00

Optimal proof systems for Propositional Logic and complete sets


Authors: Jochen Me\3ner, Jacobo Toran
Publication: 20th June 1997 11:12
Downloads: 2139


A polynomial time computable function $h:\Sigma^*\to\Sigma^*$ 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 $\gamma$ 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 $\cap$ SPARSE follow from the existence of optimal proof systems.

ISSN 1433-8092 | Imprint