Author:

• Martina Seidl
  Johannes Kepler University, Institute for Symbolic Artificial Intelligence, Austria

Abstract:

Many application problems from artificial intelligence, verification, and formal synthesis can be efficiently encoded as quantified Boolean formulas (QBFs), the extension of propositional logic with quantifiers. This extension makes the QBF decision problem PSPACE-complete (in contrast to SAT which is NP-complete).
Over the last years, much progress has been made concerning the theory and practice of QBF research. In this tutorial, we review the state of the art of QBF technology and show how to perform automated reasoning with QBFs.

Short Bio:

Prof. Martina Seidl is head of the Institute for Symbolic Artificial Intelligence at the Johannes Kepler University (JKU) in Linz, Austria. She obtained her PhD from the Vienna Technical University and her habilitation in computer science from JKU. Before becoming a full professor, she was associate professor at the Institute for Formal Models and Verification at
JKU.  Her research focuses on symbolic reasoning techniques with special emphasis on quantified Boolean formulas and applications in formal verification and symbolic artificial intelligence.