Logic and Computability (SS 2021)

Course Number IND04033UF | Sommersemester 2021

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 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. Finally, we discuss the fundamental limitations of the computing abilities of computers and discuss selected decision problems and the underlying algorithms.

The content of this lecture includes:

  • Syntax and semantics of logic formulas in propositional logic and predicate logic (first-order logic)
  • Basics of logical reasoning (natural deduction)
  • Combinational equivalence checking
  • Propositional satisfiability problem – DPLL algorithm – Resolution proofs
  • Binary Decision Diagrams
  • First-Order Theories
  • Satisfiability modulo Theories

Material

NR Date Topic Lecture Notes Slides Videos
0 2021-03-05 Administrative Information slides_0
1 2021-03-12 Propositional Logic Lecture Notes Chapter 1 slides_1 video_1
2 2021-03-19 Natural Deduction for Propositional Logic Lecture Notes Chapter 2 slides_2 video_2
3 2021-03-26 Euqivalence Checking, Normal Forms Lecture Notes Chapter 3 slides_3 video_3
4 2021-04-16 SAT Solving Lecture Notes Chapter 4 slides_4 video_4
5 2021-04-23 Binary Decision Diagrams Lecture Notes Chapter 5 slides_5 video_5
2021-05-05 16:00 Question Hour – Propositional Logic
6 2021-05-07 Predicate Logic Lecture_Notes_Chapter 6 slides_6 video_6
7 2021-05-21 Natural Deduction for Predicate Logic Lecture_Notes_Chapter 7 slides_7 video_7
8 2021-05-28 Symbolic Encoding Lecture_Notes_Chapter 8 slides_8
9 2021-06-04 Satisfiability Modulo Theory Lecture_Notes_Chapter_9 slides_9
10 2021-06-11 Summary / Training for Exam slides_10
2021-06-18 Question Hour – Predicate Logic slides_11

Material – Practicals

Number TOPIC Kick-Off Deadline (3:59 am) Assignment Bonus: Coding Example Solutions
1 Natural Deduction for Propositional Logic 2021-03-19 2021-04-16 Assignment_1 Bonus 1 Assignment 1 Solution
2 SAT Solving 2021-04-16 2021-04-30 Assignment_2 Bonus 2 Assignment 2 Solution
3 BDDs, Symbolic Encoding 2021-04-30 2021-05-21 Assignment_3 Bonus 3 Assignment_3 Solution
4 Natural Deduction for Predicate Logic 2021-05-21 2021-06-04 Assignment_4 Bonus 4 Asignment_4_Solution
5 Satisfiability Modulo Theory 2021-06-04 2021-06-18 Assignment 5 Assignment_5_Solution

The  proof rules for Natural Deduction and the Tseitin’s encoding rules can also be used during the exam and the exercise classes.

 

The upstream repository for the practical bonus assignments can be found here.

Administrative Information

For a detailed presentation of the administrative information please check the administrative slides of the first lecture.

The lecture will be held online this semester.
Ongoing communication, support, and  question hours happen online on Discord.
Please use the Discord invitation link and see our Discord Rules of Conduct to simplify the communiction during the semester.

Course Procedure

The lecture will be held in the style of a ‘flipped classroom‘. On Mondays, the students will be provided with videos, slides, and lecture-notes. The students may use the provided material to get familiar with the content of this week’s lecture. At the end of the lecture-notes, students will find examples for self-evaluations. These are examples cover both theoretically as well as practical examples in a similar way that might be ask at the final exam. The lecture takes place every Friday at 10:00-12:00. During class, we will solve these self-evaluation examples online and discuss any open questions to the topic of this week. Details for participating to the class will be sent via email to all enrolled students.

Exams

The exam for the lecture is in written form with a duration of 120 minutes. Dates for exams are set in TUGrazonline; please register there.

Exams consist of both theoretic questions and practical questions. The questions are similar to the examples and self-control questions given in the lecture notes and
the tasks given in the practical’s assignments.

 

Administrative Information – Practicals

The praticals will be held online this semester.
Ongoing communication, support, question hours, exercise classes and tests happen online on Discord.
Please use the Discord invitation link and see our Discord Rules of Conduct to simplify the communiction during the semester.

Course Procedure

During the semester, five assignments will be posted containing pen-and-paper exercises plus voluntary programming examples. Students have at least two weeks’ time to solve the assignment.

Students are required to tick the tasks they have solved on the Student Tick System. The deadline for ticking is Friday 3:59am at the day of the deadline. Submitting the programming examples will be handled via git, with the same submission deadlines. You will receive your Stics account and your repository after the registration deadline for the course has ended.

In the groups, for each of the tasks, one of the students who ticked the respective task will be selected to present his/her solution to the group.

Furthermore, there are two tests: one in the middle of the semester, one at the end.

The classes for presenting the assignments as well as test 1 and test 2 are conducted via Discord.
You will need a webcam for ID verification.
For the tests will receive an individual, randomized exam as PDF by email.
You can edit it digitally or on paper (print or plain paper, scan or photograph result and convert back to PDF). The final submission of this PDF is via TeachCenter Exam.

Time Line

Participants will be divided into eight groups:

  • Friday 1:00pm – 2:00pm (Grabner 1)
  • Friday 2:00pm – 3:00pm (Grabner 2)
  • Friday 1:00pm – 2:00pm (Peterlin 1)
  • Friday 2:00pm – 3:00pm (Peterlin 2)
  • Friday 1:00pm – 2:00pm (Pranger 1)
  • Friday 2:00pm – 3:00pm (Pranger 2)
  • Friday 1:00pm – 2:00pm (Uhl 1)
  • Friday 2:00pm – 3:00pm (Uhl 2)

Groups will start exactly at the times indicated above. (No 15 minutes delay!)

DATE TOPIC
2021-04-16 Class 1: Students defend Assignment 1
2021-04-30 Class 2: Students defend Assignment 2
2021-05-07 Test 1: Tasks similar to tasks from Assignment 1, 2
2021-05-21 Class 3: Students defend Assignment 3
2021-06-04 Class 4: Students defend Assignment 4
2021-06-18 Class 5: Students defend Assignment 5
2021-06-25 Test 2: Tasks similar to tasks from Assignment 3, 4, 5
2021-07-02 Replacement Test for Test 1 and Test 2

At every week inbetween two assignments, we will have a question hour at Discord from 1:00pm-2:00pm.

Grading

  • Achievable points of assignment 1-5: 50 Points (10 points each)
  • Achievable points from Test 1: 25 Points
  • Achievable points from Test 2: 25 Points
  • Achievable bonus Points from programming examples: 20 Points

Students need at least 25 points (=50%) from assignment 1-5.

  • Rate = points of ticked tasks + points of tests (+ bonus points from the programming examples)

If Rate…

  • >= 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

Lecturers

Bettina Könighofer
Bettina
Könighofer

PostDoc

View more