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
02 14.03 & 17.03 Horn formulas, SAT, Tseitin's transformation
03 21.03 & 24.03 natural deduction, soundness
04 28.03 & 31.03 completeness, resolution, binary decision diagrams
05 04.04 & 07.04 binary decision diagrams, predicate logic (syntax)
06 25.04 & 28.04 predicate logic (semantics), natural deduction
07 02.05 & 05.05 quantifier equivalences, unification, Skolemization
08 09.05 & 12.05 resolution, undecidability, algebraic normal forms
09 16.05 & 19.05 Post's adequacy theorem, CTL, CTL model-checking algorithm
10 23.05 & 02.06 symbolic model checking, LTL
11 30.05 & 09.06 adequacy, fairness, LTL model-checking algorithm
12 13.06 & 23.06 CTL*, SAT solving, sorting networks
13 20.06 & 30.06 sorting networks, SAT solving
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.