Logic and Computability (SS 2022)
Table of Content
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 |
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 |
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.
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
- >= 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
