Propositional Proof Complexity and Disjoint NP-Pairs II

Recent developments of cryptographic, combinatorical and complexity-theoretic techniques have opened new perspectives for the investigation of proof-theoretical

questions. Using these tools we pursue the development of a general theory for propositional proof systems. In particular, we concentrate on strong proof systems such as Frege systems, for which, in contrast to weak systems as resolution, many questions are still unresolved. In the course of our preceding project, disjoint NP-pairs proved to be an expressive tool to answer such questions, and we will try to further our understanding of these pairs.

In this project, we will focus on characteristic properties of practically relevant propositional proof systems. To this end we will model these properties using disjoint NP-pairs and wish to provide complexity-theoretic characterizations of these pairs in the lattice of all NP-pairs. We also want to use cryptographic concepts, such as

pseudo-random generators, to prove lower bounds the lengths of proofs. The ultimate goal of these investigations are lower bounds to the proof size in extended Frege systems, possibly under cryptographic assumptions.

Duration of Project

Start date: 04/2008

End date: 03/2010