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.