Subcategories
Summer 2025
Bachelor Program
| Course number | Type/hours | Semester | Title |
|---|---|---|---|
| 703026 + 703027 | VO3 + PS2 | SS 2025 | Logic |
| 703083 + 703084 | VO3 + PS2 | SS 2025 | Program Verification |
| 703141 | VU3 | SS 2025 | Term Rewriting |
Logic
Lecturers: Aart Middeldorp, Alexander Montag, Johannes Niederhauser, Daniel Ranalter, Vera Schmitt, Sven Goetzke, Harald Zankl
News: Check this site regularly for announcements; visit the content to access the slides, the homework exercises, as well as selected solutions.
Registration: Online registration for the exercises (PS) is required until 23:59 on February 21 and for the lecture (VO) until 23:59 on June 30.
Registration: Online registration is required between August 21 and September 11 (23:59) for the 2nd exam on September 25.
Registration: Online registration for the PS is required until 23:59 on February 21. Groups 1 and 6 are taught in English, groups 2, 3, 4 and 5 are taught in German.
| Date | Topics | Slides | Excercises | Solutions |
|---|---|---|---|---|
| 03.03 & 06.03 & 13.03 | propositional logic, satisfiability, validity, conjunctive normal forms | pdf (x1, x4) | ||
| 10.03 & 20.03 | Horn formulas, SAT, Tseitin's transformation | pdf (x1, x4) | ||
| 17.03 & 27.03 | natural deduction, soundness | pdf (x1, x4) | ||
| 24.03 & 03.04 | completeness, resolution, binary decision diagrams | pdf (x1, x4) | ||
| 31.03 & 10.04 | binary decision diagrams, predicate logic (syntax) | pdf (x1, x4) | ||
| 07.04 & 08.05 | predicate logic (semantics), natural deduction | pdf (x1, x4) | ||
| 28.04 & 08.05 | quantifier equivalences, unification, Skolemization | pdf (x1, x4) | ||
| 05.05 & 15.05 | resolution, undecidability, algebraic normal forms | pdf (x1, x4) | ||
| 12.05 & 22.05 | Post's adequacy theorem, CTL, CTL model-checking algorithm | pdf (x1, x4) | ||
| 19.05 & 05.06 | symbolic model checking, LTL | pdf (x1, x4) | ||
| 26.05 & 12.06 | adequacy, fairness, LTL model-checking algorithm | pdf (x1, x4) | ||
| 02.06 & 12.06 | CTL*, SAT solving, sorting networks | pdf (x1, x4) | ||
| 16.06 | SAT solving, sorting networks | pdf (x1, x4) | ||
| 23.06 | 1st exam (solution) | |||
| 25.09 | 2nd exam | |||
| 26.02 | 3rd exam |
Literature
The course is largely based on the following book:
- Michael Huth and Mark Ryan
Logic in Computer Science (second edition)
Cambridge University Press, 2007
ISBN 0-521-54310-X (paperback)
Slides as well as solutions to selected exercises will be made available online.
Program Verification
Introduction
The lecture covers the following topics:
- validation and verification
- partial correctness and termination
- automatic termination analysis
- usage of SMT-solvers
- specification of properties of programs
- verification of functional programs
- verification of imperative programs
- proof techniques: induction, invariants, generalization
Language: German
Prerequisites: Knowledge about functional programming and logic.