en | de

Logic

bachelor program

VO3 + PS2  SS 2023  703026 + 703027


Content

The course provides an introduction to logic and model checking.

Schedule

date topics slides exercises solutions
06.03 & 09.03 propositional logic, satisfiability, validity, conjunctive normal forms
13.03 & 16.03 Horn formulas, SAT, Tseitin's transformation
20.03 & 23.03 natural deduction, soundness
27.03 & 30.03 completeness, resolution, binary decision diagrams
17.04 & 20.04 binary decision diagrams, predicate logic (syntax)
24.04 & 27.04 predicate logic (semantics), natural deduction
24.04 & 04.05
08.05 & 11.05 quantifier equivalences, unification, Skolemization
15.05 & 25.05 resolution, undecidability, algebraic normal forms
22.05 & 01.06 Post's adequacy theorem, CTL, CTL model-checking algorithm
05.06 & 15.06 symbolic model checking, LTL
12.06 adequacy, fairness, LTL model-checking algorithm
19.06 & 22.06 CTL*, SAT solving
26.06 1st exam
27.09 2nd exam
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.