Bachelor Program - Logic
VO3 + PS2 SS 2026 703026 + 703027
News
Check this site regularly for announcements; visit the content page to access the slides, the homework exercises, as well as selected solutions.
From next week on the tutorium will take place on Wednesdays, 10:15 – 11:00, in RR 26.
Online registration for the PS is required until 23:59 on February 21. Groups 3 and 6 are taught in English, groups 1, 2, 4, 5 and 7 are taught in German.
Overview
Lectures
| Type | Lecturer | Room | Consultation Hours |
| VO | Aart Middeldorp | 3M07 | Monday 12:00 – 13:30 |
| TU | Aaron Gross | by arrangement | |
| PS | Luca Campa | 3M03 | Wednesday 10:00 – 11:30 |
| PS | Philipp Dablander | 3M03 | Wednesday 10:00 – 11:30 |
| PS | Alexander Montag | ÖH Technik | Monday 11:30 – 12:30 |
| PS | Johannes Niederhauser | 3M03 | Wednesday 10:00 – 11:30 |
| PS | Vera Schmitt | by arrangement |
Time & Place
The lecture (VO) starts on Monday March 2, the exercise sessions (PS) on Thursday March 5.
| Type | Lecturer | Room | Date and Time | |
| VO | Aart Middeldorp | HSB1 | Monday 08:30 – 13:30 | |
| TU | Aaron Gross | RR26 | Wednesday 10:15 - 11:00 | |
| PS | Group 1 | Alexander Montag | HS 10 | Thursday 08:15 - 09:45 |
| Group 2 | Vera Schmitt | HS 10 | Thursday 12:00 - 12:30 | |
| Group 3 | Luca Campa | HSB 4 | Thursday 08:30 - 10:00 | |
| Group 4 | Philipp Dablander | HSB 8 | Thursday 12:00 - 13:30 | |
| Group 5 | Vera Schmitt | SR 12 | Thursday 08:30 - 10:00 | |
| Group 6 | Johannes Niederhauser | HS C | Thursday 12:00 - 13:30 | |
| Group 7 | Alexander Montag | HS E | Thursday 12:00 - 13:30 |
Language
The lecture is taught in English. Exercise groups 3 and 6 are taught in English, groups 1, 2, 4, 5 and 7 are taught in German.
OLAT Links
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.
Exam
The grade for the lecture (VO) is determined by a single exam. The first opportunity is on Monday June 29, 2025, 8:30 – 11:00 in HSB 1 and 3. Online registration is required until 23:59 on Monday June 15. When preparing for the exam, you may find exams of earlier semesters useful:
Content
The course provides an introduction to logic and model checking.
Schedule
| Date | Topics | Slides | Exercises | Solutions |
| 02.03 & 05.03 & 12.03 | propositional logic, satisfiability, validity, conjunctive normal forms | PDF (x1, x4) | ||
| 09.03 & 19.03 | Horn formulas, SAT, Tseitin's transformation | PDF (x1, x4) | ||
| 16.03 & 26.03 | natural deduction, soundness | PDF (x1, x4) | ||
| 23.03 & 16.04 | completeness, resolution, binary decision diagrams | PDF (x1, x4) | ||
| 13.04 & 23.04 | binary decision diagrams, predicate logic (syntax) | PDF (x1, x4) | ||
| 20.04 & 30.04 | predicate logic (semantics), natural deduction | PDF (x1, x4) | ||
| 27.04 & 07.05 | quantifier equivalences, unification, Skolemization | PDF (x1, x4) | ||
| 04.05 & 21.05 | resolution, undecidability, algebraic normal forms | PDF (x1, x4) | ||
| 11.05 & 21.05 | Post's adequacy theorem, CTL, CTL model-checking algorithm | PDF (x1, x4) | ||
| 18.05 & 28.05 | symbolic model checking, LTL | PDF (x1, x4) | ||
| 01.06 & 11.06 | adequacy, fairness, LTL model-checking algorithm | PDF (x1, x4) | ||
| 08.06 & 18.06 | CTL*, SAT solving, sorting networks | PDF (x1, x4) | ||
| 15.06 & 25.06 | SAT solving, sorting networks | PDF (x1, x4) | ||
| 22.06 | compactness, second-order logic, first-order theories | PDF (x1, x4) | ||
| 29.06 | 1st exam | PDF (x1, x4) | ||
| 15.09 | 2nd exam | PDF (x1, x4) | ||
| 04.02 | 3rd exam | PDF (x1, x4) |
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.