en | de

Logic

bachelor program

VO3 + PS2  SS 2024  703026 + 703027


Content

The course provides an introduction to logic and model checking.

Schedule

date topics slides exercises solutions
04.03 & 07.03 propositional logic, satisfiability, validity, conjunctive normal forms pdf (x1, x4) pdf pdf
11.03 & 14.03 Horn formulas, SAT, Tseitin's transformation pdf (x1, x4) pdf pdf
18.03 & 21.03 natural deduction, soundness pdf (x1, x4) pdf pdf
08.04 & 11.04 completeness, resolution, binary decision diagrams pdf (x1, x4) pdf pdf
15.04 & 18.04 binary decision diagrams, predicate logic (syntax) pdf (x1, x4) pdf pdf
22.04 & 25.04 predicate logic (semantics), natural deduction pdf (x1, x4) pdf pdf
29.04 & 02.05 quantifier equivalences, unification, Skolemization pdf (x1, x4) pdf pdf
06.05 & 16.05 resolution, undecidability, algebraic normal forms pdf (x1, x4) pdf pdf
13.05 & 23.05 Post's adequacy theorem, CTL, CTL model-checking algorithm pdf (x1, x4) pdf pdf
27.05 & 06.06 symbolic model checking, LTL pdf (x1, x4) pdf pdf
03.06 & 06.06 adequacy, fairness, LTL model-checking algorithm pdf (x1, x4) pdf pdf
10.06 & 13.06 CTL*, SAT solving, sorting networks pdf (x1, x4) pdf pdf
17.06 & 20.06 SAT solving, sorting networks pdf (x1, x4) pdf pdf
24.06 1st exam (solution)
20.09 2nd exam (solution)
26.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.