Logic and Computability (SS 2024)

Course Number IND04033UF | Sommersemester 2024

Content

In this course, you will learn to understand logic formulas, to use concise mathematical notations, to formulate and solve problems in formal languages, and to reason with logics manually and algorithmically. We will use powerful tools, so called SMT solvers, that are able to quickly solve complex problems involving constraints over integers, reals, first-order logic predicates, list, and other data types. We will teach logic proof systems, and you will gain the ability to construct logic proofs on your own and you will master common proof techniques of computer science.

The content of this lecture includes:

  • Syntax and semantics of logic formulas in propositional logic and predicate logic (first-order logic)
  • Propositional satisfiability problem – DPLL algorithm – Resolution proofs
  • Satisfiability modulo Theories - DPLL(T)
  • Basics of logical reasoning (natural deduction)
  • Binary Decision Diagrams
  • Temporal Logic
  • Introduction to the SMT Solver Z3

Material

The students will be provided with videos, slides, lecture notes and a questionnaire. The material will be online before the corresponding lecture.

NR Date Topic Lecture Notes Slides Questionnaire Video
0 2024-03-01 Administrative Information Slides 0
1 2024-03-08 Propositional Logic and SAT Solving Lecture Notes 1 Lecture Notes 2 Slides 1 Slides 2 Questionnaire 1 Solutions Questionnaire 2 Solutions Video 1 Video 2
2 2024-03-15 Binary Decision Diagrams Lecture Notes 3 Slides 3 Questionnaire 3 Solutions Video 3
3 2024-03-22 Natural Deduction for Propositional Logic Lecture Notes 4 Slides 4 Questionnaire 4 Solutions Video 4 Recording
4 2024-04-12 Combinatorial Equivalence Checking Introduction to Z3 I Lecture Notes 5 Example Repository Slides 5 Slides 6 Questionnaire 5 Solutions Questionnaire 6 Solutions Recording
5 2024-04-19 Predicate Logic Introduction to Z3 II Lecture Notes 7 Example Repository Slides 7 Slides 6 contd. Questionnaire 7 Solutions Recording
6 2024-04-26 Natural Deduction for Predicate Logic
7 2024-03-05 Satisfiability Modulo Theory
8 2024-05-17 Satisfiability Modulo Theory
9 2024-05-24 Z3
10 2024-05-31 Transition Systems and Temporal Logic
11 2024-06-07 Decidability
12 2024-06-14 Question Hour
13 2024-06-16 Probabilistic Temporal Logic and BDDs
The proof rules for Natural Deduction and the Tseitin's encoding rules can also be used during the exam and the exercise classes. Solutions for the questions from the questionnaire will be released here. You can watch videos explaining the topics discussed in the lecture in the TUbe.

Practicals

Number Topic Kick-Off Deadline Assignment Solutions
1 SAT Solving and Binary Decision Diagrams 2024-03-08 2024-03-20 Assignment 1 [DPLL Table] Solutions 1
2 Natural Deduction for Propositional Logic 2024-03-22 2024-04-10 Assignment 2 Solutions 2
3 Equivalence Checking and Predicate Logic 2024-04-12 2024-04-24 Assignment 3
4 Natural Deduction for Predicate Logic 2024-05-03 2024-05-15
5 Satisfiability Modulo Theory 2024-05-17 2024-05-22
6 Z3 Programming Assignment 2024-04-12 2024-06-05 Upstream Repository
Note that the exercises discussed in the practicals are also contained in the respective chapter of the questionnaire.

Administrative Information

Administrative Information - Lecture

Questionnaire Students will be provided with a questionnaire. These questions cover the theoretical aspects of the lecture as well as practical examples. The questions for a particular topic will be published on Monday before the corresponding lecture. The questions at the exam are a subset of the questions of the questionnaire. Course Procedure The lecture takes place every Friday at 10:15-12:00 at i13. During class, we will interactively work out the theory and solve questions from the questionnaire. Exams Dates for exams will be set via TUGrazonline, please register there. Exams will have a duration of 90 minutes and there will be at least 3 possible dates for exams each semester. The questions at the exam are a subset of the questions of the questionnaire. Communication - Discord Please use the Discord invitation link to simplify the communication during the semester.

Administrative Information - Practicals

Course Procedure In total, we will have 5 pen-and-paper assignments and practical programming assignments. For the five pen-and-paper assignments you will practice the basic decisions procedures, basic algorithms, and perform simple proofs by hand. The practical programming assignments will cover simple examples using the python library of z3. The assignments will be discussed by students during live blackboard sessions in class. Please register for any of the 10 groups. Students are required to tick the tasks they have solved via the TeachCenter. The deadline for ticking is Thursday 23:59am before the respective practical session. Students will be randomly selected during class to present their solutions. Submitting the programming examples will be handled via git. You will receive your repository after the registration deadline for the course has ended. The attendance of practical classes is compulsory. For justified reasons (sickness), exceptions can be made. In such cases, students have to tick and upload their solutions in time (according to the deadline of the assignment) and have to present their solutions in a replacement interview that will be held in the following week, on Thursday at 2:00pm. If students are not able to explain their solution or their solution is completely wrong, students may lose either 50% or 100% of the points of that assignment. Minor errors or typos will not lead to any point reductions. Grading for the Practicals
  • Assignment 1 - 5: 15 points each
  • Programming Assignment: 25 points
  • Assignments may include bonus points.
If Points…
  • >= 87.5%: (1) Sehr Gut / Excellent
  • >= 75.0%: (2) Gut / Good
  • >= 62.5%: (3) Befriedigend / Satisfactory
  • >= 50.0%: (4) Genügend / Sufficient
  • >= 00.0%: (5) Nicht Genügend / Insufficient
Communication - Discord Please use the Discord invitation link to simplify the communication during the semester. For any questions, please contact either Stefan Pranger or Bettina Könighofer.

Lecture Dates

Date Begin End Location Event Type Comment
2024/04/25 14:00 15:00 Seminarraum IST Abhaltung KU fix/
2024/04/25 14:00 15:00 Seminarraum Abhaltung KU fix/
2024/04/25 14:00 15:00 Seminarraum Abhaltung KU fix/
2024/04/25 14:00 15:00 VTU Seminarraum Abhaltung KU fix/
2024/04/25 14:00 15:00 Seminarraum CGV Abhaltung KU fix/
2024/04/25 14:00 15:00 Abhaltung KU fix/
2024/04/25 15:00 16:00 Seminarraum IST Abhaltung KU fix/
2024/04/25 15:00 16:00 Seminarraum Abhaltung KU fix/
2024/04/25 15:00 16:00 Seminarraum CGV Abhaltung KU fix/
2024/04/25 15:00 16:00 Seminarraum Abhaltung KU fix/
2024/04/25 15:00 16:00 Abhaltung KU fix/
2024/04/25 15:00 16:00 VTU Seminarraum Abhaltung KU fix/
2024/04/26 10:00 12:00 HS i13 Abhaltung VO fix/
2024/05/02 14:00 15:00 Abhaltung KU fix/
2024/05/02 14:00 15:00 HS i14 Abhaltung KU fix/
2024/05/02 14:00 15:00 HS FSI 1 "Magna Steyr Hörsaal" Abhaltung KU fix/
2024/05/02 14:00 15:00 Seminarraum Abhaltung KU fix/
2024/05/02 14:00 15:00 Seminarraum Abhaltung KU fix/
2024/05/02 14:00 15:00 Seminarraum CGV Abhaltung KU fix/
2024/05/02 15:00 16:00 HS FSI 1 "Magna Steyr Hörsaal" Abhaltung KU fix/
2024/05/02 15:00 16:00 Seminarraum Abhaltung KU fix/
2024/05/02 15:00 16:00 Seminarraum CGV Abhaltung KU fix/
2024/05/02 15:00 16:00 Seminarraum Abhaltung KU fix/
2024/05/02 15:00 16:00 HS i14 Abhaltung KU fix/
2024/05/02 15:00 16:00 Abhaltung KU fix/
2024/05/03 10:00 12:00 HS i13 Abhaltung VO fix/
2024/05/16 14:00 15:00 Seminarraum CGV Abhaltung KU fix/
2024/05/16 14:00 15:00 Abhaltung KU fix/
2024/05/16 14:00 15:00 HS i14 Abhaltung KU fix/
2024/05/16 14:00 15:00 HS FSI 1 "Magna Steyr Hörsaal" Abhaltung KU fix/
2024/05/16 14:00 15:00 Seminarraum Abhaltung KU fix/
2024/05/16 14:00 15:00 Seminarraum Abhaltung KU fix/
2024/05/16 15:00 16:00 Abhaltung KU fix/
2024/05/16 15:00 16:00 HS FSI 1 "Magna Steyr Hörsaal" Abhaltung KU fix/
2024/05/16 15:00 16:00 Seminarraum Abhaltung KU fix/
2024/05/16 15:00 16:00 Seminarraum Abhaltung KU fix/
2024/05/16 15:00 16:00 Seminarraum CGV Abhaltung KU fix/
2024/05/16 15:00 16:00 HS i14 Abhaltung KU fix/
2024/05/17 10:00 12:00 HS i13 Abhaltung VO fix/
2024/05/23 14:00 15:00 Seminarraum Abhaltung KU fix/
2024/05/23 14:00 15:00 Abhaltung KU fix/
2024/05/23 14:00 15:00 HS i14 Abhaltung KU fix/
2024/05/23 14:00 15:00 HS FSI 1 "Magna Steyr Hörsaal" Abhaltung KU fix/
2024/05/23 14:00 15:00 Seminarraum Abhaltung KU fix/
2024/05/23 15:00 16:00 Seminarraum CGV Abhaltung KU fix/
2024/05/23 15:00 16:00 HS i14 Abhaltung KU fix/
2024/05/23 15:00 16:00 Abhaltung KU fix/
2024/05/23 15:00 16:00 HS FSI 1 "Magna Steyr Hörsaal" Abhaltung KU fix/
2024/05/23 15:00 16:00 Seminarraum Abhaltung KU fix/
2024/05/23 15:00 16:00 Seminarraum Abhaltung KU fix/
2024/05/24 10:00 12:00 HS i13 Abhaltung VO fix/
2024/05/31 10:00 12:00 HS i13 Abhaltung VO fix/
2024/06/06 14:00 15:00 VTU Seminarraum Abhaltung KU fix/
2024/06/06 14:00 15:00 Seminarraum Abhaltung KU fix/
2024/06/06 14:00 15:00 Seminarraum CGV Abhaltung KU fix/
2024/06/06 14:00 15:00 Seminarraum Abhaltung KU fix/
2024/06/06 14:00 15:00 HS i14 Abhaltung KU fix/
2024/06/06 14:00 15:00 Seminarraum IST Abhaltung KU fix/
2024/06/06 15:00 16:00 Seminarraum Abhaltung KU fix/
2024/06/06 15:00 16:00 Seminarraum Abhaltung KU fix/
2024/06/06 15:00 16:00 Seminarraum CGV Abhaltung KU fix/
2024/06/06 15:00 16:00 HS i14 Abhaltung KU fix/
2024/06/06 15:00 16:00 VTU Seminarraum Abhaltung KU fix/
2024/06/06 15:00 16:00 Seminarraum CGV Abhaltung KU fix/
2024/06/06 15:00 16:00 Seminarraum IST Abhaltung KU fix/
2024/06/07 10:00 12:00 HS i13 Abhaltung VO fix/
2024/06/14 10:00 12:00 HS i13 Abhaltung VO fix/
2024/06/19 16:00 19:00 HS FSI 1 "Magna Steyr Hörsaal" Abhaltung VO fix/Voluntary Trainings-evening
2024/06/21 10:00 12:00 HS i13 Abhaltung VO fix/

Lecturers

Bettina Könighofer
Bettina
Könighofer

Assistant Professor

View more
Stefan Pranger
Stefan
Pranger

PhD Student

View more