Disjoint NP-Pairs from Propositional Proof Systems

  • Olaf Beyersdorff
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3959)


For a proof system P we introduce the complexity class DNPP(P) of all disjoint NP-pairs for which the disjointness of the pair is efficiently provable in the proof system P. We exhibit structural properties of proof systems which make the previously defined canonical NP-pairs of these proof systems hard or complete for DNPP(P). Moreover we demonstrate that non-equivalent proof systems can have equivalent canonical pairs and that depending on the properties of the proof systems different scenarios for DNPP(P) and the reductions between the canonical pairs exist.


Polynomial Time Proof System Modus Ponens Propositional Formula Automate Theorem Prove 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Atserias, A., Bonet, M.L.: On the automatizability of resolution and related propositional proof systems. In: Computer Science Logic, 16th International Workshop, pp. 569–583 (2002)Google Scholar
  2. Beyersdorff, O.: Representable disjoint NP-pairs. In: Proc. 24th Conference on Foundations of Software Technology and Theoretical Computer Science, pp. 122–134 (2004)Google Scholar
  3. Beyersdorff, O.: Disjoint NP-pairs from propositional proof systems. Technical Report TR05-083, Electronic Colloquium on Computational Complexity (2005)Google Scholar
  4. Bonet, M.L., Pitassi, T., Raz, R.: Lower bounds for cutting planes proofs with small coefficients. The Journal of Symbolic Logic 62(3), 708–728 (1997)zbMATHCrossRefMathSciNetGoogle Scholar
  5. Bonet, M.L., Pitassi, T., Raz, R.: On interpolation and automatization for Frege systems. SIAM Journal on Computing 29(6), 1939–1967 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  6. Buss, S.R.: Bounded Arithmetic. Bibliopolis, Napoli (1986)zbMATHGoogle Scholar
  7. Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. The Journal of Symbolic Logic 44, 36–50 (1979)zbMATHCrossRefMathSciNetGoogle Scholar
  8. Glaßer, C., Selman, A.L., Sengupta, S.: Reductions between disjoint NP-pairs. In: Proc. 19th Annual IEEE Conference on Computational Complexity, pp. 42–53 (2004)Google Scholar
  9. Glaßer, C., Selman, A.L., Sengupta, S., Zhang, L.: Disjoint NP-pairs. SIAM Journal on Computing 33(6), 1369–1416 (2004)zbMATHCrossRefMathSciNetGoogle Scholar
  10. Glaßer, C., Selman, A.L., Zhang, L.: Canonical disjoint NP-pairs of propositional proof systems. In: Proc. 30th International Symposium on the Mathematical Foundations of Computer Science, pp. 399–409 (2005)Google Scholar
  11. Grollmann, J., Selman, A.L.: Complexity measures for public-key cryptosystems. SIAM Journal on Computing 17(2), 309–335 (1988)zbMATHCrossRefMathSciNetGoogle Scholar
  12. Homer, S., Selman, A.L.: Oracles for structural properties: The isomorphism problem and public-key cryptography. Journal of Computer and System Sciences 44(2), 287–301 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  13. Köbler, J., Messner, J., Torán, J.: Optimal proof systems imply complete sets for promise classes. Information and Computation 184, 71–92 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  14. Krajíček, J.: Bounded Arithmetic, Propositional Logic, and Complexity Theory. In: Encyclopedia of Mathematics and Its Applications, vol. 60. Cambridge University Press, Cambridge (1995)Google Scholar
  15. Krajíček, J.: Interpolation theorems, lower bounds for proof systems and independence results for bounded arithmetic. The Journal of Symbolic Logic 62(2), 457–486 (1997)zbMATHCrossRefMathSciNetGoogle Scholar
  16. Krajíček, J.: Dual weak pigeonhole principle, pseudo-surjective functions, and provability of circuit lower bounds. The Journal of Symbolic Logic 69(1), 265–286 (2004)zbMATHCrossRefMathSciNetGoogle Scholar
  17. Krajíček, J., Pudlák, P.: Propositional proof systems, the consistency of first order theories and the complexity of computations. The Journal of Symbolic Logic 54, 1963–1979 (1989)Google Scholar
  18. Krajíček, J., Pudlák, P.: Quantified propositional calculi and fragments of bounded arithmetic. Zeitschrift für mathematische Logik und Grundlagen der Mathematik 36, 29–46 (1990)zbMATHCrossRefGoogle Scholar
  19. Krajíc̃ek, J., Pudlák, P.: Some consequences of cryptographical conjectures for S12 and EF. Information and Computation 140(1), 82–94 (1998)CrossRefMathSciNetGoogle Scholar
  20. Pudlák, P.: Lower bounds for resolution and cutting planes proofs and monotone computations. The Journal of Symbolic Logic 62, 981–998 (1997)zbMATHCrossRefMathSciNetGoogle Scholar
  21. Pudlák, P.: On reducibility and symmetry of disjoint NP-pairs. Theoretical Computer Science 295, 323–339 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  22. Razborov, A.A.: On provably disjoint NP-pairs. Technical Report TR94-006, Electronic Colloquium on Computational Complexity (1994)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Olaf Beyersdorff
    • 1
  1. 1.Institut für InformatikHumboldt-Universität zu BerlinBerlinGermany

Personalised recommendations