Logic and Computability (WS 2025/26)
Table of Content
Content
In this course, you will learn to understand logical formulas, use concise mathematical notation, formulate and solve problems in formal languages, and reason with logic both manually and algorithmically. We will use powerful tools, called SMT solvers, which can quickly solve complex problems involving constraints over integers, reals, first-order logic predicates, lists, and other data types. You will also be introduced to logical proof systems, gain the ability to construct proofs on your own, and master common proof techniques used in computer science.The content of this lecture includes:
- Syntax and semantics of logical formulas in propositional logic and first-order logic
- The propositional satisfiability problem: DPLL algorithm and resolution proofs
- Satisfiability Modulo Theories (SMT) and the DPLL(T) framework
- Basics of logical reasoning (natural deduction)
- Binary Decision Diagrams (BDDs)
- Introduction to the SMT solver Z3
Material
The students will be provided with videos, slides, lecture notes, and a questionnaire.| NR | Date | Topic | Lecture Notes | Slides | Questionnaire | Video |
|---|---|---|---|---|---|---|
| 0 | 2025-10-06 | Administrative Information + Teaser | Slides 0 | |||
| 1 | 2025-10-13 | Propositional Logic | ||||
| 2 | 2025-10-20 | Natural Deduction for Propositional Logic | ||||
| 3 | 2025-10-27 | SAT Solving | ||||
| 4 | 2025-11-03 | Equivalence Checking + Symbolic Encoding | ||||
| 5 | 2025-11-10 | Binary Decision Diagrams | ||||
| 6 | 2025-11-17 | Predicate Logic | ||||
| 7 | 2025-11-24 | Natural Deduction for Predicate Logic | ||||
| 8 | 2025-12-01 | Solving SMT with Z3 | ||||
| 9 | 2025-12-15 | Satisfiability Modulo Theories I | ||||
| 10 | 2026-01-12 | Satisfiability Modulo Theories II | ||||
| 11 | 2026-01-19 | Decidability | ||||
| 12 | 2026-01-26 | Training Exam | ||||
| 13 | 2026-01-28 | Training Evening |
Practicals - Materials and Timeline
| Number | Topic | Kick-Off | Deadline | Assignment | Solutions |
|---|---|---|---|---|---|
| 1 | Natural Deduction for Propositional Logic | 2025-10-20 | 2025-10-26 | ||
| 2 | SAT Solving | 2025-10-27 | 2025-11-02 | ||
| 3 | BDDs and Equivalence Checking | 2025-11-03 | 2025-11-16 | ||
| 4 | Predicate Logic | 2025-11-17 | 2025-11-23 | ||
| 5 | Natural Deduction for Predicate Logic | 2025-11-24 | 2025-11-30 | ||
| P1 | Z3 Programming | 2025-12-01 | 2025-12-14 | ||
| 6 | Satisfiability Modulo Theories | 2025-12-15 | 2026-01-18 | ||
| P2 | Z3 Programming | 2025-12-01 | 2026-01-25 |
Administrative Information
Administrative Information - Lecture
Course Procedure
Lectures take place every Monday from 12:15–14:00 in room i12.
-
Exceptions will be announced under Lecture Dates below or via TUGrazonline.
-
Classes are interactive: we will work through the theory together and solve selected questionnaire problems.
-
Students will receive a questionnaire containing both theoretical and practical questions related to the lecture.
-
Exam questions will be selected from this questionnaire, though they may be slightly modified (e.g., adjusted formulas or reordered multiple-choice options).
Exams
-
Exam dates are scheduled via TUGrazonline; please make sure to register there.
-
Each exam lasts 90 minutes.
-
There will be at least three exam dates per semester.
Communication
For smooth communication throughout the semester, please join our Discord server via this link.
Administrative Information - Practicals
Course Procedure
There will be six pen-and-paper assignments and two practical programming assignments. In the pen-and-paper assignments, you will practice basic decision procedures and algorithms, as well as perform simple proofs by hand. The programming assignments will involve small examples using the Python library of Z3.
Practical Groups
Assignments will be discussed by students in live blackboard sessions during class. Please register for one of the ten regular groups. In addition, two special groups are available: Early Bird and Late Bird. If you cannot attend the regular sessions (15:00–16:00 or 16:00–17:00), you may contact the lecturers to request a place in either the Early Bird group (08:00–09:00) or the Late Bird group (18:00–19:00).
Absence from Practical Classes
Attendance at practical classes is compulsory. Exceptions may be granted for justified reasons (e.g., illness). In such cases, students must tick and upload their solutions on time (according to the assignment deadline) and present them in a replacement interview, which will be held the following Monday.
Submission of Pen-and-Paper Assignments
Students must tick the tasks they have solved via the TeachCenter. The deadline for ticking is Sunday, 23:59, before the respective practical session. During class, students will be randomly selected to present their solutions. Marking a task as solved in the TeachCenter counts as entering the examination for the practicals.
Submission of Programming Assignments
Programming assignments will be submitted via Git. You will receive your repository after the registration deadline for the course has passed. The first programming assignment will be discussed in class, with students randomly selected to present their solutions. The second programming assignment will be assessed through individual interviews at the end of the semester.
Grading
If students are unable to explain their solution, or if the solution is completely incorrect, they may lose up to 100% of the points for that assignment. Minor errors or typos will not result in point deductions.
-
Students in the SC curriculum 2025 are required to complete the 2 ECTS version of the practicals.
-
Students in the SC curriculum 2024 or earlier may instead complete the 1 ECTS version, which is identical to the 2 ECTS version but without the programming assignments.
Grading Scheme for the 2 ECTS Practicals
-
Assignments 1–6: 6 × 10 points
-
Programming Assignments 1–2: 10 + 30 points
-
Assignments may include bonus points.
| Points | Grade | Description |
|---|---|---|
| ≥ 87.5 | (1) Sehr Gut | Excellent |
| ≥ 75.0 | (2) Gut | Good |
| ≥ 62.5 | (3) Befriedigend | Satisfactory |
| ≥ 50.0 | (4) Genügend | Sufficient |
| < 50.0 | (5) Nicht Genügend | Insufficient |
Grading Scheme for the 1 ECTS Practicals
-
Assignments 1–6: 6 × 10 points
-
Assignments may include bonus points.
| Points | Grade | Description |
|---|---|---|
| ≥ 52.5 | (1) Sehr Gut | Excellent |
| ≥ 45.0 | (2) Gut | Good |
| ≥ 37.5 | (3) Befriedigend | Satisfactory |
| ≥ 30.0 | (4) Genügend | Sufficient |
| < 30.0 | (5) Nicht Genügend | Insufficient |
Usage of Generative AI
We follow the general TU Graz guidelines on the use of generative AI.
Contact
For any questions, please contact Bettina Könighofer or Stefan Pranger.
Lecture Dates
| Date | Begin | End | Location | Event | Type | Comment |
|---|---|---|---|---|---|---|
| 2025/10/16 | 08:00 | 10:00 | HS i2 | Abhaltung | VO | fix/ |
| 2025/10/16 | 08:00 | 10:00 | HS i2 | Abhaltung | VO | fix/ |
| 2025/10/20 | 12:00 | 14:00 | HS i12 "DynaTrace Hörsaal" | Abhaltung | VO | fix/ |
| 2025/10/30 | 09:00 | 11:00 | HS A | Abhaltung | VO | fix/ |
| 2025/11/03 | 12:00 | 14:00 | HS i12 "DynaTrace Hörsaal" | Abhaltung | VO | fix/ |
| 2025/11/10 | 12:00 | 14:00 | HS i12 "DynaTrace Hörsaal" | Abhaltung | VO | fix/ |
| 2025/11/17 | 12:00 | 14:00 | HS i12 "DynaTrace Hörsaal" | Abhaltung | VO | fix/ |
| 2025/11/24 | 12:00 | 14:00 | HS i12 "DynaTrace Hörsaal" | Abhaltung | VO | fix/ |
| 2025/12/01 | 12:00 | 14:00 | HS i12 "DynaTrace Hörsaal" | Abhaltung | VO | fix/ |
| 2025/12/15 | 12:00 | 14:00 | HS i12 "DynaTrace Hörsaal" | Abhaltung | VO | fix/ |
| 2026/01/12 | 12:00 | 14:00 | HS i12 "DynaTrace Hörsaal" | Abhaltung | VO | fix/ |
| 2026/01/19 | 12:00 | 14:00 | HS i12 "DynaTrace Hörsaal" | Abhaltung | VO | fix/ |
| 2026/01/26 | 12:00 | 14:00 | HS i12 "DynaTrace Hörsaal" | Abhaltung | VO | fix/ |
| 2026/01/28 | 16:00 | 19:00 | HS i9 | Abhaltung | VO | fix/ |
Lecturers
Könighofer
Assistant Professor