# Logic and Computability (WS 2024/25)

### 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
- 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 | Video |
---|---|---|---|---|---|---|

0 | 2024-10-07 | Administrative Information | Slides 0 | |||

1 | 2024-10-13 | Propositional Logic | ||||

2 | 2024-10-21 | Natural Deduction for Propositional Logic | ||||

3 | 2024-11-08 | SAT Solving | ||||

4 | 2024-11-11 | Symbolic Encoding | ||||

5 | 2024-11-18 | Binary Decision Diagrams | ||||

6 | 2024-11-25 | Predicate Logic and Introduction to Z3 | ||||

7 | 2024-12-02 | Natural Deduction for Predicate Logic | ||||

8 | 2024-12-09 | Satisfiability Modulo Theory | ||||

9 | 2024-12-16 | Z3 Christmas Special | ||||

10 | 2025-01-13 | Satisfiability Modulo Theory | ||||

11 | 2025-01-20 | Soundness and Completeness |

## Practicals

Number | Topic | Kick-Off | Deadline | Assignment | Solutions |
---|---|---|---|---|---|

1 | Natural Deduction for Propositional Logic | 2024-10-21 | 2024-10-27 | ||

2 | SAT Solving | 2024-11-08 | 2024-11-17 | ||

3 | Binary Decision Diagrams and Symbolic Encoding | 2024-11-18 | 2024-11-24 | ||

4 | Predicate Logic | 2024-11-25 | 2024-12-01 | ||

5 | Natural Deduction for Predicate Logic | 2024-12-02 | 2024-12-08 | ||

6 | Satisfiability Modulo Theory | 2025-01-13 | 2025-01-19 | ||

7 | Z3 Programming Assignment | TBA | TBA |

## 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. The questions for a particular topic will be published on Monday before the corresponding lecture. The questions**at the exam**are a

**subset of the questions of the questionnaire**.

#### Course Procedure

The lecture takes place every Monday at 12:15-14:00 at i12. For exceptions, see the lecture dates below or on TUG online. During class, we will interactively work out the theory and solve questions from the questionnaire.#### Exams

Dates for exams will be set via TUGrazonline, please register there. Exams will have a duration of 90 minutes and there will be at least 3 possible dates for exams each semester. The questions**at the exam**are a

**subset of the questions of the questionnaire**.

#### Communication - Discord

Please use the Discord invitation link to simplify the communication during the semester.**Administrative Information - Practicals**

#### Course Procedure

In total, we will have 6 pen-and-paper assignments and one practical programming assignment. For the six pen-and-paper assignments you will practice the basic decisions procedures, basic algorithms, and perform simple proofs by hand. The practical programming assignment will cover simple examples using the python library of z3. 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 Sunday, 23:59 before the respective practical session. Students will be randomly selected during class to present their solutions. The practical assignments will (can) be done in groups of two. You will discuss your solutions with your tutor at the end of the semester. 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 Monday. 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 - 6: 13
- Programming Assignment: 22
- 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

#### Communication - Discord

Please use the Discord invitation link to simplify the communication during the semester. For any questions, please contact either Stefan Pranger or Bettina Könighofer.## Lecture Dates

Date | Begin | End | Location | Event | Type | Comment |
---|---|---|---|---|---|---|

2024/10/14 | 12:00 | 14:00 | HS i12 "DynaTrace Hörsaal" | Abhaltung | VO | fix/Voluntary Trainings-evening |

2024/10/14 | 12:00 | 14:00 | HS i12 "DynaTrace Hörsaal" | Abhaltung | VO | fix/ |

2024/10/21 | 12:00 | 14:00 | HS i12 "DynaTrace Hörsaal" | Abhaltung | VO | fix/ |

2024/10/28 | 12:15 | 14:00 | HS i12 "DynaTrace Hörsaal" | Abhaltung | VO | fix/ |

2024/11/04 | 12:00 | 14:00 | HS i12 "DynaTrace Hörsaal" | Abhaltung | VO | fix/ |

2024/11/08 | 12:00 | 14:00 | HS i7 | Abhaltung | VO | fix/ |

2024/11/11 | 12:00 | 14:00 | HS P2 | Abhaltung | VO | fix/ |

2024/11/18 | 12:00 | 14:00 | HS i12 "DynaTrace Hörsaal" | Abhaltung | VO | fix/ |

2024/11/25 | 12:00 | 14:00 | HS i12 "DynaTrace Hörsaal" | Abhaltung | VO | fix/ |

2024/12/02 | 12:00 | 14:00 | HS i12 "DynaTrace Hörsaal" | Abhaltung | VO | fix/ |

2024/12/09 | 12:00 | 14:00 | HS i12 "DynaTrace Hörsaal" | Abhaltung | VO | fix/ |

2024/12/16 | 12:00 | 14:00 | HS i12 "DynaTrace Hörsaal" | Abhaltung | VO | fix/ |

2025/01/13 | 12:00 | 14:00 | HS i12 "DynaTrace Hörsaal" | Abhaltung | VO | fix/ |

2025/01/20 | 12:00 | 14:00 | HS i12 "DynaTrace Hörsaal" | Abhaltung | VO | fix/ |

2025/01/27 | 12:00 | 14:00 | HS i12 "DynaTrace Hörsaal" | Abhaltung | VO | fix/ |

2025/01/29 | 16:00 | 18:00 | HS i9 | Abhaltung | VO | fix/ |