Graduiertenkolleg: Methods for Discrete Structures

Deutsche Forschungsgemeinschaft
faculty | junior-faculty | postdocs | students | associate students | former students | former associate students
locations | Term schedule | history
predoc-courses | schools | block-courses | workshops

Monday Lecture and Colloquium

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

Meena Mahajan - CIT Campus, Chennai, India

Lower bound techniques for QBF proof systems

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



Letzte Aktualisierung: 26.01.2018