Logic and Computability (SS 2022)

Course Number IND04033UF and IND05034UF | Sommersemester 2022

Lecturers

Bettina Könighofer

Lukas Posch

Teaching Assistants

Paul Gollob

Amel Smajic

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 Videos Slides Questionnaire
0 2022-03-04 Administrative Information Slides 0
1 2022-03-11 Propositional Logic Lecture Notes 1 Video 1 Slides 1 Questionnaire 1
2 2022-03-18 Natural Deduction for Propositional Logic Lecture Notes 2 Video 2 Slides 2 Questionnaire 2
3 2022-03-25 Equivalence Checking, Normal Forms Lecture Notes 3 Video 3 Slides 3 Questionnaire 3
4 2022-04-01 SAT Solving Lecture Notes 4 Video 4 Slides 4 Questionnaire 4
6 2022-04-29 Binary Decision Diagrams Lecture Notes 5 Video 5 Slides 5 Questionnaire 5
7 2022-05-06 Predicate Logic Lecture Notes 6 Video 6 Slides 6 Questionnaire 6
8 2022-05-13 Natural Deduction for Predicate Logic Lecture Notes 7 Video 7 Slides 7 Questionnaire 7
9 2022-05-20 Modelling Systems Lecture Notes 8 Video 8 Slides 8 Questionnaire 8
10 2022-06-03 Satisfiability Modulo Theory Lecture Notes 9 Video 9 Slides 9 Questionnaire 9
12 2022-06-17 Temporal Logic Lecture Notes 10 Video 10 Slides 10 Questionnaire 10
11 2022-06-10 Question Hour Example Exam Solutions

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.

The final version of the questionnaire is available here. A version with the solutions discussed in the lecture is available here.

Practicals

Number TOPIC Kick-Off Deadline (3:59 am) Assignment Solutions
1 Natural Deduction for Propositional Logic 2022-03-18 2022-04-01 Assignment 1 Solutions 1
2 SAT Solving 2022-04-01 2022-04-29 Assignment 2 [DPLL Table] Solutions 2
3 BDDs, Symbolic Encoding 2022-04-29 2022-05-13 Assignment 3 Solutions 3
4 Natural Deduction for Predicate Logic 2022-05-13 2022-06-03 Assignment 4 Solutions 4
5 Satisfiability Modulo Theory 2022-06-03 2022-06-17 Assignment 5 Solution 5

Note that the exercises discussed in the practicals are also contained in the respective chapter of the questionnaire.

Programming Bonus

All material for the programming bonus examples, including introductions and videos, can be found in the upstream repository here.

Administrative Information

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

Administrative Information – Lecture

Course Procedure

The lecture will be held in the style of a ‘flipped classroom‘. On Mondays, the students will be provided with videos, slides, questions, and lecture notes. The students may use the provided material to get familiar with the content of that week’s lecture.

The lecture takes place every Friday at 10:15-12:00 at i13, video recordings will be provided and uploaded after class. During class, we will interactively solve the questions of the questionnaire labelled with [Lecture] and discuss any open questions.

Questionnaire

Students will be provided with a questionnaire. These questions cover the theoretical aspects of the lecture as well as practical examples. Questions within the questionnaire will have one of the following labels:

  • [Lecture] Questions that will solved during the lecture on Friday. Solutions will be provided by us after the lecture.
  • [Practicals] Questions part of the assignments of the practicals. Solutions will be provided by us after the corresponding practicals.
  • [Self-Assessment] Questions for self-assessment. Students are encouraged to post solutions (git) and discuss solutions (Discord). Details will be provided soon.

The questions for a particular topic will be published on Monday before the corresponding lecture.

The questions that will be asked at the exam will be a subset of the questions of the questionnaire.

Exams

Dates for exams will be set via TUGrazonline, please register there. Exams will have a duration of 120 minutes and there will be at least 3 possible dates for exams each semester.

The questions that will be asked at the exam will be a subset of the questions of the questionnaire.

Communication – Discord

Please use the Discord invitation link to simplify the communiction during the semester.

Administrative Information – Practicals

Course Procedure

During the semester, five assignments will be made available on this site containing pen-and-paper exercises. Students have at least two weeks to solve the assignment. The exercises will be part of the questionnaire and will be labelled with [Practicals]

The assignments will be discussed by students during live blackboard sessions in class or video sessions via Discord. Please register for any of the 10 groups (6 of which will be held on campus, 4 via Discord).

Students are required to tick and upload the tasks they have solved via the TeachCenter. The deadline for ticking is Friday 3:59am of the respective practical session. Students will be randomly selected during class to present their solutions.

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, Friday, 1pm, via Discord.

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.

In Fridays where no practical class will be held, we offer a voluntary question hour via Discord from 13:00 to 14:00.

In addition to the mandatory pen-and-paper exercises, there will be voluntary programming examples which will let you collect bonus points. Submitting the programming examples will be handled via git. You will receive your repository after the registration deadline for the course has ended.

Grading for the Practicals

  • Achievable points of assignment 1-5: 100 Points (20 points each)
  • Achievable bonus Points from programming examples: 20 Points
  • Rate = points of ticked tasks + 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

Communication – Discord

Please use the Discord invitation link to simplify the communication during the semester.

For any questions regarding the exercise, please contact either Stefan Pranger or Bettina Könighofer.

Lecturers

Bettina Könighofer
Bettina
Könighofer

Assistant Professor

View more
Lukas Posch
Lukas
Posch


View more

Teaching Assistants

Paul Gollob
Paul
Gollob


View more
Amel Smajic
Amel
Smajic


View more