Abstract
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 in [5] and in order to compare the relative strength 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íček and Pudlák [13,12] proved 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 gave a condition implying the existence of optimal proof systems (a related concept to the one of p-optimal systems). In this paper we improve this result obtaining 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 deterministic 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 then the class UP (and 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.
Preview
Unable to display preview. Download preview PDF.
References
E. Allender. Invertible functions. Ph.D. dissertation, Georgia Institute of Technology, 1985.
J. L. Balcázar, J. Diaz, and J. Gabarró. Structural Complexity I, volume 11 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1988.
S. Buss. Lectures on Proof Theory. Tech Report No. SOCS-96.1, McGill University, 1996. (http://www.cs.mcgill.ca/tdenis/TR.96.1.ps.gz) 2
J. Cai and L. Hemachandra. On the power of parity polynomial time. Mathematical Systems Theory 23, pp. 95–106, 1990.
S. Cook and R. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic 44, pp. 36–50, 1979.
J. Hartmanis. Generalized Kolmogorov complexity and the structure of feasible computations. In Proceedings of the 24th IEEE Symposium on Foundations of Computer Science (FOCS'83), pp. 439–445, 1983
J. Hartmanis and L. Hemachandra Complexity classes without machines: On complete languages for UP. Theoretical Computer Science, 58, pp. 129–142, 1988.
J. Hartmanis and J. Yesha. Computation times of NP sets of different densities. Theoretical Computer Science, 34, pp. 17–32, 1984.
L. Hemaspaandra, S. Jain and N. Vereshchagin. Banishing robust Turing completeness. Int. Journal of Foundations of Computer Science, 4, pp. 245–265, 1993.
R. Karp and R. Lipton. Some connections between nonuniform and uniform complexity classes. In Proceedings of the 12th ACM Symposium on Theory of Computing, pp. 302–309, 1980.
J. Krajiĉek. Bounded Arithmetic, Propositional Logic and Complexity Theory Cambridge University Press 1995.
J. Krajiĉek and P. Pudlák. Propositional proof systems, the consistency of first order theories and the complexity of computations. Journal of Symbolic Logic 54, pp. 1063–1079, 1989.
P. Pudlák. On the length of proofs of finitistic consistency statements in first order theories. Logic Colloquium'84 (J. B. Paris et al., editors), North-Holland, Amsterdam, pp. 165–196, 1986
A. A. Razborov. On provably disjoint NP-pairs. Technical Report RS-94-36, Basic Research in Computer Science Center, Aarhus, 1994.
U. Schöning.On random reductions from sparse sets to tally sets.Information Processing Letters, 46, pp. 239–241, 1993.
A. Urquhart. The complexity of propositional proofs. Bulletin of Symbolic Logic 1, pp. 425–467, 1995.
L. Valiant. The relative complexity of checking and evaluating. Information Processing Letters, 5, pp. 20–23, 1976.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag
About this paper
Cite this paper
Messner, J., Torán, J. (1998). Optimal proof systems for propositional logic and complete sets. In: Morvan, M., Meinel, C., Krob, D. (eds) STACS 98. STACS 1998. Lecture Notes in Computer Science, vol 1373. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028583
Download citation
DOI: https://doi.org/10.1007/BFb0028583
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64230-5
Online ISBN: 978-3-540-69705-3
eBook Packages: Springer Book Archive