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.

2021S, VU, 4.0h, 6.0EC
  • TUWEL Online-Kurs verfügbar ab: 04.03.2021 09:00.

Merkmale

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

Lernergebnisse

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-Reasoning.

Due to current COVID-19 pandemic, the course will take place entirely online

- with all lectures made available as pre-recorded lectures, on the day of the respective lecture;

- with four live Q&A sessions via Zoom. 

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.

Methoden

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

There will be 4 homeworks,  handed out online. 
Exercises/homework solutions will be discussed during the live Q&A sessions, via Zoom.

Prüfungsmodus

Schriftlich

Weitere Informationen

The course is held block, within 8 weeks, with 2 lectures a week

The course will start on March 4, 9am, with an introductory lecture summarizing general course information. The kick-off on March 4, 9am will be held live, via Zoom, at the following link: 

https://tuwien.zoom.us/j/92898893549?pwd=MFh2WmJXejBRZjlVcjJ2VFJyZUtJUT09

The first proper lecture is on March 9, 9:15-10:45, as a pre-recorded lecture. 

 



Vortragende

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Do.09:00 - 10:0004.03.2021 https://tuwien.zoom.us/j/92898893549?pwd=MFh2WmJXejBRZjlVcjJ2VFJyZUtJUT09Automated Deduction - Kick-off Lecture, General Information
Di.09:00 - 11:0009.03.2021 - 04.05.2021 Pre-recorded lectureAutomated Deduction - Pre-recorded Lecture
Do.09:00 - 11:0011.03.2021 - 06.05.2021 Pre-recorded lectureAutomated Deduction - Pre-recorded Lecture
Do.11:00 - 12:3025.03.2021 Online, live on ZoomQ&A 1 - Discussions and Recap
Do.11:00 - 12:3022.04.2021 Online, live on ZoomQ&A 2 - Discussions and Recap
Do.11:00 - 12:3006.05.2021 Online, live on ZoomLecture 14 and Q&A 3 - Completeness of Superposition and Recap
Automated Deduction - Einzeltermine
TagDatumZeitOrtBeschreibung
Do.04.03.202109:00 - 10:00 https://tuwien.zoom.us/j/92898893549?pwd=MFh2WmJXejBRZjlVcjJ2VFJyZUtJUT09Automated Deduction - Kick-off Lecture, General Information
Di.09.03.202109:00 - 11:00 Pre-recorded lectureAutomated Deduction - Pre-recorded Lecture
Do.11.03.202109:00 - 11:00 Pre-recorded lectureAutomated Deduction - Pre-recorded Lecture
Di.16.03.202109:00 - 11:00 Pre-recorded lectureAutomated Deduction - Pre-recorded Lecture
Do.18.03.202109:00 - 11:00 Pre-recorded lectureAutomated Deduction - Pre-recorded Lecture
Di.23.03.202109:00 - 11:00 Pre-recorded lectureAutomated Deduction - Pre-recorded Lecture
Do.25.03.202109:00 - 11:00 Pre-recorded lectureAutomated Deduction - Pre-recorded Lecture
Do.25.03.202111:00 - 12:30 Online, live on ZoomQ&A 1 - Discussions and Recap
Di.13.04.202109:00 - 11:00 Pre-recorded lectureAutomated Deduction - Pre-recorded Lecture
Do.15.04.202109:00 - 11:00 Pre-recorded lectureAutomated Deduction - Pre-recorded Lecture
Di.20.04.202109:00 - 11:00 Pre-recorded lectureAutomated Deduction - Pre-recorded Lecture
Do.22.04.202109:00 - 11:00 Pre-recorded lectureAutomated Deduction - Pre-recorded Lecture
Do.22.04.202111:00 - 12:30 Online, live on ZoomQ&A 2 - Discussions and Recap
Di.27.04.202109:00 - 11:00 Pre-recorded lectureAutomated Deduction - Pre-recorded Lecture
Do.29.04.202109:00 - 11:00 Pre-recorded lectureAutomated Deduction - Pre-recorded Lecture
Di.04.05.202109:00 - 11:00 Pre-recorded lectureAutomated Deduction - Pre-recorded Lecture
Do.06.05.202109:00 - 11:00 Pre-recorded lectureAutomated Deduction - Pre-recorded Lecture
Do.06.05.202111:00 - 12:30 Online, live on ZoomLecture 14 and Q&A 3 - Completeness of Superposition and Recap

Leistungsnachweis

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 online exam.The date and time of the final written exam will be announced later. 

LVA-Anmeldung

Von Bis Abmeldung bis
03.02.2021 09:00 10.03.2021 23:59 11.03.2021 23:59

Curricula

Literatur

For slides and other material see the TUWEL course.

Weitere Informationen

Sprache

Englisch