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.
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.
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:
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 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.
The course is held blocked, within 8 weeks, with 2 pre-recorded 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.
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, by uploading scanned solutions on TUWEL. Students are required to identify themselves online, upon entering the online written exam. The online written exam will likely be monitored via Zoom and students are required to be online during the entire slot of the online exams (further details are available on the TUWEL page of the course).
The final written exam will take place as an online written exam in June 2021. The following two exam slots are available:
Please register, via TISS, and participate in only one of the above two slots.
For slides and other material see the TUWEL course.