What's important about Quantified Boolean Formulas?

Leroy Chew, University of Leeds. Part of the algebra, logic and algorithms seminar series

As many expressive logics are undecidable, propositional logic is readily used in computer science.  One can augment propositional logic with Boolean quantifiers to get the logic known as Quantified Booleans Formulas (QBF).  Recently, there has been an increase in focus on QBF solving and an attempt to reconcile practice with theoretical results, particularly from proof complexity.  In this talk I'll be explaining why we should study QBF and what are the important results that it yields.