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.