Quantified Boolean Formulas: Solving and Proofs

  Quantified Boolean Formulas: Solving and Proofs Vorlesung im Sommersemester 2021
Verantwortlicher Dr. Joshua Blinkhorn
Leistungspunkte (ECTS credits) 2 SWS Vorlesung (3 LP)
geeignet für Master und Bachelor
Zeiten Diese Vorlesung wird online über BBB angeboten.

Vorlesungstermine:
Freitags 12-14 Uhr
Inhalte We will study state-of-the-art solving techniques and associated proof systems for quantified Boolean formulas (QBF), an important test case for algorithmic progress in automated reasoning.
No prerequsite knowledge is essential for this course, but the lecture `Alogorithmisches Beweisen' would be an ideal foundation.
We will cover the following topics:

- Existential and universal quantification in Boolean logic
- QBF decision procedures and solvers
- QBF proof systems based on resolution
- Analysis of solvers using proof complexity
- Universal expansion and universal reduction (QCDCL)
- Dedicated lower bound techniques and hard formulas
- Syntactic and semantic variable dependence
Sprache  Diese Vorlesung wird auf Englisch stattfinden.