Humboldt-Universität zu Berlin - Faculty of Mathematics and Natural Sciences - Complexity and Cryptography

Propositional Proof Complexity and Disjoint NP-Pairs

DFG Research Project


Project supported by Deutsche Forschungsgemeinschaft (DFG), Germany.

Duration: April 2006 to March 2008


Project Members:  Johannes Köbler, Olaf Beyersdorff


Research background

Propositional proof complexity is an active field of research combining methods from complexity theory and mathematical logic. During recent years most of the research activity has been directed towards the understanding of weak propositional proof systems like resolution. In comparison, rather limited information is available about strong systems like Frege systems and their extensions.
This project aims towards a development of a general theory of strong propositional proof systems. For the analysis of these systems we
combine new methods from computational complexity, cryptography, and logic which have been successfully developed during the recent years. More specifically, these methods include

  • the use of pseudorandom generators in propositional proof complexity,
  • the investigation of the class of disjoint NP-pairs, and
  • the correspondence between propositional proof systems and theories of bounded arithmetic.


Our major aims in the project are lower bounds to the size of propositional proofs in strong systems under suitable cryptographic or complexity-theoretic assumptions. A second objective is the characterization of these strong systems and their properties by disjoint NP-pairs.