Monday, February 5, 2018
Technische Universität Berlin
Institut für Mathematik
Straße des 17. Juni 136
10623 Berlin
room MA 041
Lecture - 14:15
Abstract:
How do we prove that a false QBF is inded false? How big a proof is
needed? The special case when all quantifiers are existential is the
well-studied setting of propositional proof complexity. Expectedly,
universal quantifiers change the game significantly. Several proof
systems have been designed in the last couple of decades to handle
QBFs. We'd like to show proof-size lower bounds in these systems.
Some lower bound paradigms from propositional proof complexity can be
extended, others can't. A new paradigm with no analogue in the
propositional world has emerged in the form of strategy extraction,
allowing for transfer of circuit lower bounds, as well as obtaining
independent genuine QBF lower bounds based on a semantic cost measure.
This talk will provide a broad overview of some of these developments.
Colloquium - 16:00
Abstract: