en | de

Logic

bachelor program

VO3 + PS2  SS 2022  703026 + 703027


Content

The course provides an introduction to logic and model checking.

Schedule

week date topics slides exercises solutions
01 07.03 & 10.03 propositional logic, satisfiability, validity, conjunctive normal forms pdf (x1, x4) pdf pdf
02 14.03 & 17.03 Horn formulas, SAT, Tseitin's transformation pdf (x1, x4) pdf pdf
03 21.03 & 24.03 natural deduction, soundness pdf (x1, x4) pdf pdf
04 28.03 & 31.03 completeness, resolution, binary decision diagrams pdf (x1, x4) pdf pdf
05 04.04 & 07.04 binary decision diagrams, predicate logic (syntax) pdf (x1, x4) pdf pdf
06 25.04 & 28.04 predicate logic (semantics), natural deduction pdf (x1, x4) pdf pdf
07 02.05 & 05.05 quantifier equivalences, unification, Skolemization pdf (x1, x4) pdf pdf
08 09.05 & 12.05 resolution, undecidability, algebraic normal forms pdf (x1, x4) pdf pdf
09 16.05 & 19.05 Post's adequacy theorem, CTL, CTL model-checking algorithm pdf (x1, x4) pdf pdf
10 23.05 & 02.06 symbolic model checking, LTL pdf (x1, x4) pdf pdf
11 30.05 & 09.06 adequacy, fairness, LTL model-checking algorithm pdf (x1, x4) pdf pdf
12 13.06 & 23.06 CTL*, SAT solving, sorting networks pdf (x1, x4) pdf pdf
13 20.06 & 30.06 sorting networks, SAT solving pdf (x1, x4) pdf pdf
27.06 1st exam (solution)
27.09 2nd exam (solution)
23.02 3rd exam

Literature

The course is largely based on the following book: Slides as well as solutions to selected exercises will be made available online. Recordings of the lectures are available from OLAT.