Logic and Computability (SS 2023)
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 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 | |
|---|---|---|---|---|---|---|
| 0 | 2023-03-03 | Administrative Information | Slides 0 | |||
| 1 | 2023-03-10 | Introduction to Z3 | Lecture 1 ( + z3 Examples) | Questionnaire 1 Solutions | ||
| 2 | 2023-03-24 | Propositional and Predicate Logic | Lecture Notes 2 | Slides 2 | Questionnaire 2 Solutions 2 | |
| 3 | 2023-03-31 | SAT Procedures - DPLL | Lecture Notes 3 | Slides 3 Solutions | Questionnaire 3 Solutions 3 | |
| 4 | 2023-04-21 | Natural Deduction for Propositional Logic | Lecture Notes 4 | Slides 4 | Questionnaire 4 Solutions 4 | |
| 5 | 2023-04-28 | Predicate Logic | Lecture Notes 5 | Slides 5 | Questionnaire 5 Solutions 5 | |
| 6 | 2023-04-28 | Natural Deduction for Predicate Logic - Part 1 | Lecture Notes 6 | Slides 6 | Questionnaire 6 Solutions 6 | |
| 6 | 2023-05-05 | Natural Deduction for Predicate Logic - Part 2 | Lecture notes 6 (see above) | Slides 6-Part2 | Questionnaire 6 (see above) | |
| 7 | 2023-05-05 | Satisfiability Modulo Theories | Lecture Notes 7 | Slides 7 | Questionnaire 7 Solutions 7 | |
| 7 | 2023-05-12 | Binary Decision Diagrams | Lecture Notes 8 | Slides 8 | Questionnaire 8 Solutions 8 | |
| 8 | 2023-05-26 | Equivalence Checking | Lecture Notes 9 | Slides 9 | Questionnaire 9 Solutions 9 | |
| 9 | 2023-06-02 | Symbolic Encoding | Lecture Notes 10 | Slides 10 | Questionnaire 10 Solutions 10 | |
| 9 | 2023-06-02 | Temporal Logic | Lecture Notes 11 | Slides 11 | Questionnaire 11 Solutions 11 | |
| 10 | 2023-06-16 | Probabilistic Temporal Logic and BDDs | Slides 12 |
Practicals
| Number | Topic | Kick-Off | Deadline | Assignment | Solutions |
|---|---|---|---|---|---|
| 1 | Programming Assignment 1 | 2023-03-10 | 2023-03-16 | Assignment 1 | |
| 2 | Programming Assignment 2 | 2023-03-17 | 2023-03-23 | Assignment 2 | |
| 3 | Programming Assignment 3 | 2023-03-24 | 2023-03-30 | Assignment 3 | |
| 4 | SAT Solving | 2023-03-31 | 2023-04-20 | Assignment 4 [DPLL Table] | Solutions 4 |
| 5 | Natural Deduction for Propositional Logic | 2023-04-21 | 2023-04-27 | Assignment 5 | Solutions 5 |
| 6 | Predicate Logic and Natural Deduction for Predicate Logic | 2023-04-28 | 2023-05-04 | Assignment 6 | Solutions 6 |
| 7 | Natural Deduction for Predicate Logic and Eager Encoding | 2023-05-05 | 2023-05-11 | Assignment 7 | Solutions 7 |
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. Questions within the questionnaire will have one of the following labels:- [Lecture] Questions that will be solved during the lecture on Friday. Solutions will be provided by us after the lecture.
- [Practicals] These questions form the practical assignments. Solutions will be provided by us after the corresponding practical class.
- [Self-Assessment] These questions are for self-assessment.
Administrative Information - Practicals
Course Procedure In total, we will have 7 practical assignments. The first three assignments will be simple programming exercises using the Python API of the SMT solver Z3. The next four assignments are pen-and-paper assignments to practice the basic decisions procedures algorithms and to perform simple proofs by hand. 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. 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: 10 points
- Assignment: 2-7: 15 points each
- Assignments may include bonus 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
Lecturers
Könighofer
Assistant Professor