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

Propositional Proof Complexity and Disjoint NP-Pairs (2)

DFG Research Project


Project supported by Deutsche Forschungsgemeinschaft (DFG), Germany.

Duration: April 2008 to March 2010


Project Members:  Johannes Köbler, Olaf Beyersdorff, Sebastian Müller


Research background

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.