Speaker: Ilario Bonacina
, KTH Royal Institute of Technology
Title: Frege systems for Quantified Boolean Logic
A longstanding and informal belief in the proof complexity community asserts a close connection between progress in circuit complexity lower bounds and progress in proof size lower bounds for propositional proof systems, that is proof systems for propositional Boolean formulas. Although some results in propositional proof complexity are inspired by techniques and results in circuit complexity, no formal connection between the two fields has been established so far. In this talk we describe a general hierarchy of proof systems for Quantified Boolean Formulas (QBF) and we give a formal connection between circuit complexity lower bunds and proof size lower bounds in such systems. As consequences, using the state-of-the-art circuit complexity separations and lower bounds, we are able to prove separations and proof size lower bounds for QBF proof systems that in the propositional case correspond to major open problems.
This talk is based on a joint work with O. Beyersdorff and L. Chew.