184.774 Automated Deduction
Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.
Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.

2023S, VU, 4.0h, 6.0EC


  • Semesterwochenstunden: 4.0
  • ECTS: 6.0
  • Typ: VU Vorlesung mit Übung
  • Format der Abhaltung: Hybrid


Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage...

- Methoden von Automated Deduction zu erklaeren und benuetzen, wie zB SAT/SMT solving und superposition-based first-order theorem proving. 

The course will take place in teh following setting: 

- In-class kick-off event on March 2, 2023; 

- Pre-recorded lectures: all lectures will be made available as pre-recorded lectures, on the day of the respective lecture;

- In-class discussions: there will be four Q&A sessions, to be held in-person only. These sessions are meant to recap lecture material covered by respective pre-recorded lectures, disucss exercises/homework solutions, and provide feedback on students' questions. 

Lecture recordings and slides will be posted online on the TUWEL site of the course, and course-related discussions will be monitored online on TUWEL. 


The reasoning power that computational logic offers brings new perspectives in the field of program verification. This course is about computational logic, with particular focus on algorithmic and automated methods for proving logical properties.

The course aims at teaching attendees algorithmic techniques and fundamental results in automated deduction. Student will also use state-of-the-art theorem provers for proving logical properties.

Inhalt der Lehrveranstaltung

The course focuses on specialised algorithms for reasoning in various fragments of first-order logics, such as propositional logic, combination of ground theories, and full first-order logic with equality. We will address both the theoretical and practical aspects for using and implementing (semi-)decisions procedures of various logics.

The tentative list of topics covered by the course is below:

  • propositional and first-order logic;
  • satisfiability checking in propositional logic (splitting, DPLL, randomized algorithms);
  • satisfiability checking in the theory of arithmetic, uninterpreted functions and arrays;
  • satisfiability checking the the combination of theories (SMT);
  • validity proving in first-order logic (superposition theorem proving). 

The course will address transformation to normal forms, DPLL, SAT-solving, SMT-solving, resolution, unification, superposition, redundancy checking, and  experiments with theorem provers.

The course will also include hands-on sessions using the SAT solver MINISAT, the SMT solver Z3 and the first-order theorem prover VAMPIRE.


There will be two pre-recorded lectures a week, with lecture slides accompanying the lectures. 

There will be 4 homeworks,  handed out online. 

Exercises/homework solutions, as well as additional, course-related material will be discussed during the in-class discussions. 



Weitere Informationen

The complete course information (lecture material, news, discussions) is only available on the TUWEL site of the course

The course is held blocked, within 8 weeks, during March 2-May 11, 2023. 

The course starts on March 2, 9:15am, with an introductory kick-off lecture summarizing general course information. The kick-off on March 2 is held in-class.

The first proper lecture is on March 7, 9:15-10:45, as a pre-recorded lecture. There will be 2 pre-recorded lectures a week


Vortragende Personen


LVA Termine

Do.09:00 - 11:0002.03.2023EI 11 Geodäsie HS - INF LVA Automated Deduction - Kick-off
Do.09:00 - 11:0016.03.2023EI 11 Geodäsie HS - INF LVA Automated Deduction - QA1
Do.09:00 - 11:0030.03.2023EI 11 Geodäsie HS - INF LVA Automated Deduction - QA2
Do.09:00 - 11:0027.04.2023EI 11 Geodäsie HS - INF LVA Automated Deduction - QA3
Do.09:00 - 11:0011.05.2023EI 11 Geodäsie HS - INF LVA Automated Deduction - QA4
Mo.09:00 - 12:0022.05.2023EI 11 Geodäsie HS - INF Automated Deduction - Written Exam
Mo.09:00 - 12:0012.06.2023EI 11 Geodäsie HS - INF Automated Deduction - Written Exam


The course grade will be based on four written homework assignments and a written exam.

Homework assignments count for 40% of the course grade.

The exam will take place as an open-book written exam. 


Von Bis Abmeldung bis
06.02.2023 09:00 12.03.2023 23:59 12.03.2023 23:59


066 011 DDP Computational Logic (Erasmus-Mundus) Keine Angabe
066 931 Logic and Computation Gebundenes Wahlfach
066 937 Software Engineering & Internet Computing Gebundenes Wahlfach
066 938 Technische Informatik Gebundenes Wahlfach
860 GW Gebundene Wahlfächer - Technische Mathematik Gebundenes Wahlfach


For slides and other material see the TUWEL course.

Weitere Informationen