Logic and Computability

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
• Decidability, Halteproblem
• 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
5	2021-04-23	Binary Decision Diagrams, Symbolic Encoding
	2021-04-30	Question Hour – Propositional Logic
6	2021-05-07	Predicate Logic
7	2021-05-21	Natural Deduction for Predicate Logic
8	2021-05-28	Satisfiability Modulo Theory – 1
9	2021-06-04	Satisfiability Modulo Theory – 2
10	2021-06-11	Decidability
	2021-06-18	Question Hour – Predicate Logic

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
2	SAT Solving	2021-04-16	2021-04-30
3	BDDs, Symbolic Encoding	2021-04-30	2021-05-21
4	Natural Deduction for Predicate Logic	2021-05-21	2021-06-04
5	Satisfiability Modulo Theory	2021-06-04	2021-06-18

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

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

Lecture Dates

Date	Begin	End	Location	Event	Type	Comment
2021/04/16	10:00	12:00	HS i13	Abhaltung	VO	fix/
2021/04/23	10:00	12:00	HS i13	Abhaltung	VO	fix/
2021/04/23	10:00	12:00	HS i13	Abhaltung	VO	fix/
2021/04/30	10:00	12:00	HS i13	Abhaltung	VO	fix/
2021/05/21	10:00	12:00	HS i13	Abhaltung	VO	fix/
2021/05/28	10:00	12:00	HS i13	Abhaltung	VO	fix/
2021/06/04	10:00	12:00	HS i13	Abhaltung	VO	fix/
2021/06/11	10:00	12:00	HS i13	Abhaltung	VO	fix/
2021/06/18	10:00	12:00	HS i13	Abhaltung	VO	fix/

Lecturers