Content
The module provides an introduction into the theory and practice of decision procedures. The course 703620 covers the theory of decision procedures and includes the following topics:
- propositional logic (SAT)
- equality logic with uninterpreted functions (EUF)
- linear arithmetic (LIA and LRA)
- quantified boolean formulas (QBF)
- Nelson-Oppen combination method
- Presburger arithmetic
- tree automata
- first-order theory of rewriting
- problem solving with SAT encodings
- algorithms for equality logic
- first-order syntactic and equational unification (specifically, with respect to associative and commutative function symbols)
- nonreachability
Schedule
| week | date | slides (TDP) | slides (PDP) | sources | exercises | solutions | remarks |
|---|---|---|---|---|---|---|---|
| 1 | 05.03 & 09.03 | ||||||
| 2 | 12.03 & 16.03 | ||||||
| 3 | 19.03 & 23.03 | ||||||
| 4 | 09.04 & 13.04 | ||||||
| 5 | 16.04 & 20.04 | ||||||
| 6 | 23.04 & 27.04 | ||||||
| 7 | 30.04 & 04.05 | ||||||
| 8 | 07.05 & 11.05 | ||||||
| 9 | 14.05 & 18.05 | ||||||
| 10 | |||||||
| 11 | 28.05 & 01.06 | ||||||
| 12 | 04.06 & 08.06 | exam (PDP) | |||||
| 13 | 11.06 & 15.06 | ||||||
| 14 | 18.06 & 22.06 | ||||||
| 15 | 25.06 & 29.06 | exam (TDP) |