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

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.