en | de

# Decision Procedures (WM 5)

## master program

VO2 + VO1 + PS2  SS 2018  703620 + 703621 + 703622

### 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
The course 703621 is about the usage and/or implementation of exemplary decision procedures, including the following topics:
• 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 pdf (1, 4) pdf (1, 4) archive pdf
2 12.03 & 16.03 pdf (1, 4) pdf (1, 4) archive pdf
3 19.03 & 23.03 pdf (1, 4) pdf (1, 4) archive pdf pdf
4 09.04 & 13.04 pdf (1, 4) pdf (1, 4) archive pdf pdf
5 16.04 & 20.04 pdf (1, 4) pdf (1, 4) archive pdf pdf
6 23.04 & 27.04 pdf (1, 4) pdf (1, 4) archive pdf
7 30.04 & 04.05 pdf (1, 4) pdf (1, 4) archive pdf pdf
8 07.05 & 11.05 pdf (1, 4) pdf (1, 4) archive pdf
9 14.05 & 18.05 pdf (1, 4) pdf (1, 4) pdf
10 21.05 & 25.05 pdf pdf
11 28.05 & 01.06 pdf (1, 4) pdf (1, 4) pdf pdf
12 04.06 & 08.06 pdf (1, 4) pdf exam (PDP)
13 11.06 & 15.06 pdf (1, 4) pdf
14 18.06 & 22.06 pdf (1, 4) pdf
15 25.06 & 29.06 pdf exam (TDP)