Kann über Anerkennungsmodul belegt werden und gibt 3 ECTS/LP.
1.Termin: 23.4.21
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
|
