Logic and Computability (WS 2026/27)

Content

<WORK IN PROGRESS. THIS WEBSITE DOES NOT PROVIDE THE CORRECT INFORMATION FOR WS26>   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	2026-10-05	Introduction
1	2026-10-12	Propositional Logic (+ Z3 Tutorial I)
2	2026-10-19	Natural Deduction for Propositional Logic
3	2026-11-09	Equivalence Checking (+ Z3 Tutorial II)
4	2026-11-16	SAT Solving with DPLL
5	2026-11-23	Binary Decision Diagrams + Symbolic Encoding
6	2026-11-30	Predicate Logic (+ Z3 Tutorial III)
7	2026-12-07	Natural Deduction for Predicate Logic
8	2026-12-14	SMT Theory
9	2027-01-11	SMT Solving (Eager / Lazy Encoding, DPLL[T])
10	2027-01-18	Advanced Topics
11	2027-01-25	Question Hour
12	202701-28	Exam Training Event

The proof rules for Natural Deduction and the Tseitin's encoding rules can be used during the exam and in the exercise classes. You can watch videos explaining the topics covered in the lecture on TUbe.

Practicals - Materials

Number	Main Topic	Kick-Off	Deadline	Points	Assignment
1	Propositional Logic, Z3 Basics	12.10.	18.10	9
2	Natural Deduction for Propositional Logic	19.10.	08.11.	9
3	Problem Encoding, Z3 Basics II	09.11.	15.11.	9
4	SAT Solving with DPLL	16.11.	22.11.	9
5	Binary Decision Diagrams	23.11.	29.11.	9
6	Predicate Logic	30.11.	06.12.	9
7	Natural Deduction for Predicate Logic	07.12.	13.12.	9
8	SMT Solving with Z3	30.11.	10.01.	28
9	Satisfiability Modulo Theories	11.01.	18.01.	9

Assignment 8 will include mandatory assignment interviews, which will take place during the week of January 11-15.  

Administrative Information

Contact & Additional Support

For any kind of questions, you may contact the course instructor team via e-mail: lac.isec [at] mlist.tugraz.at

Optional support is also available via Discord (link). Please note that Discord is a third-party service not affiliated with TU Graz, and data may be processed outside the EU. Therefore, please do not share personal or sensitive information there. Discord is entirely optional, alternatively you can:

1. Ask questions during practical sessions (KU).
2. Ask questions before, during or after the lecture.
3. Schedule office hours with the course instructor team via e-mail.
4. Attend the in-person question and exercise sessions.

Usage of Generative AI

We follow the general TU Graz guidelines on the use of generative AI.

Administrative Information - Lecture

Course Procedure

Lectures take place every Monday from 12:15–14:00 in HS 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.

Administrative Information - Practicals

Course Procedure

There will be 9 assignments, which will include:

• applying decision procedures and algorithms presented in the lectures,
• carrying out simple proofs by hand, and
• solving problems using the Z3 Python library.

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

1. notify the course team (lac.isec [at] mlist.tugraz.at),
2. tick and upload their solutions on time (according to the assignment deadline), and
3. present them in a replacement interview, which will be held the following Monday.

Submission of 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.

Students must be able to correctly explain their solutions and the reasoning behind them. If they are unable to do so, they may lose up to 100% of the points for the entire assignment sheet. Incorrect solutions may also lead to point deductions.

<<TODO: What about submitting Assignments with z3?>>

Grading

Lecture Dates

Date	Begin	End	Location	Event	Type	Comment
2026/10/05	10:00	12:00	ICK1130H	CLASS	VO	CLASS/
2026/10/12	10:00	12:00	ICK1130H	CLASS	VO	CLASS/
2026/10/19	10:00	12:00	ICK1130H	CLASS	VO	CLASS/
2026/11/09	11:00	13:00	ICK1130H	CLASS	VO	CLASS/
2026/11/16	11:00	13:00	ICK1130H	CLASS	VO	CLASS/
2026/11/23	11:00	13:00	ICK1130H	CLASS	VO	CLASS/
2026/11/30	11:00	13:00	ICK1130H	CLASS	VO	CLASS/
2026/12/07	11:00	13:00	ICK1130H	CLASS	VO	CLASS/
2026/12/14	11:00	13:00	ICK1130H	CLASS	VO	CLASS/
2027/01/11	11:00	13:00	ICK1130H	CLASS	VO	CLASS/
2027/01/18	11:00	13:00	ICK1130H	CLASS	VO	CLASS/
2027/01/25	11:00	13:00	ICK1130H	CLASS	VO	CLASS/

Lecturers