en | de

Logic

bachelor program

VO3 + PS2  WS 2018/2019  703026 + 703027


Content

The course provides an introduction to logic and model checking.

Schedule

lecture date topics
1 01.10 & 04.10 propositional logic, satisfiability, validity, conjunctive normal forms
2 08.10 & 11.10 Horn formulas, SAT, Tseitin's transformation
3 15.10 & 18.10 natural deduction, soundness
4 22.10 & 25.10 completeness, resolution, binary decision diagrams
5 29.10 & 01.11 binary decision diagrams, algebraic normal forms, functional completeness
6 05.11 & 08.11 Post's adequacy theorem, SAT solving, sorting networks
7 12.11 & 15.11 sorting networks, SAT solving
8 19.11 & 22.11 linear-time temporal logic, adequacy
9 26.11 & 29.11 branching-time temporal logic, adequacy, CTL model-checking algorithm
10 03.12 & 06.12 fairness, CTL*, symbolic model checking
11 10.12 & 13.12 predicate logic (syntax and semantics), natural deduction
12 07.01 & 10.01 natural deduction, quantifier equivalences, unification
13 14.01 & 17.01 Skolemization, resolution, undecidability
14 21.01 & 24.01 first-order theories, Gödel's incompleteness theorem, SMT
15 28.01 1st exam

Literature

The course is largely based on the following book: Slides as well as solutions to selected exercises will be made available online.