Automated Deduction (TU Wien, SS 2019)

Course code: 184.774
Course acronym: ADuct
Course type: Lectures + Exercises (VU), 6 ETCS
Lecturer: Laura Kovács
Language of teaching: English

Course evaluation survey: Please answer the five questions in this form and return it to us in an anonymized version.


Course Code and Registration

This course is designed for Master students. Interested PhD students may also take this course.
If you need more information about the course, please contact us at laura.kovacs@tuwien.ac.at.

If you are interested in this course, please register to the course by sending an email to laura.kovacs@tuwien.ac.at.


Course Calendar

Event Date and time Room Topic Online material
Lecture 1 Thursday, March 7, 9:15-10:45 EI 3 Sahulka HS Introduction
Course outlines
Propositional logic and SAT
Slides
Slides (without animation)
Lecture 2 Tuesday, March 12, 10:15-11:45 EI 8 Poetzl HS Splitting
Polarities and pure atoms
Slides
Slides (without animation)
Lecture 3 Thursday, March 14, 9:15-10:45 EI 3 Sahulka HS Normal forms and CNF
DPLL
Using a SAT solver
Slides
Slides (without animation)
Lecture 4 NO LECTURE on Tuesday, March 19 EI 8 Poetzl HS
Lecture 5 Thursday, March 21, 9:15-10:45 EI 3 Sahulka HS Satisfiability and randomization
Satisfiability of Horn clauses
Slides
Slides (without animation)
Lecture 6 Tuesday, March 26, 10:15-11:45 EI 8 Poetzl HS First-order logic and theories
Satisfiabilty modulo theories (SMT)
Theory of equality
Slides
Slides (without animation)
Lecture 7 Thursday, March 28, 9:15-10:45 EI 3 Sahulka HS Theory of equality and congruence closure Slides
Slides (without animation)
Lecture 8 Tuesday, April 2, 10:15-11:45 EI 8 Poetzl HS SMT and non-unit clauses
Theory of arrays
SMT in combination of theories
Slides
Slides (without animation)
Lecture 9 Thursday, April 4, 9:15-10:45 EI 3 Sahulka HS SMT in combination of theories (cntd)
Running an SMT solver
First-order theorem proving - an example
Slides
Slides (without animation)
Lecture 10 Tuesday, April 9, 10:15-11:45 EI 8 Poetzl HS First-order logic and TPTP
Inference Systems
Selection functions
Saturation algorithms
Slides
Slides (without animation)
Lecture 11 Thursday, April 11, 9:15-10:45 EI 3 Sahulka HS Fair saturation algorithms
Redundancy elimination
Slides
Slides (without animation)
Lecture 12 Tuesday, April 30, 10:15-11:45 EI 8 Poetzl HS Equality
Ground superposition
Slides
Slides (without animation)
Lecture 13 Thursday, May 2, 9:15-10:45 EI 3 Sahulka HS Completeness of superposition with redundancy
- guest lecture by Andrei Voronkov
Slides
Slides (without animation)
Lecture 14 Tuesday, May 7, 10:15-11:45 EI 8 Poetzl HS Unification and lifting Slides
Slides (without animation)
Lecture 15
(last lecture)
Thursday, May 9, 9:15-10:45 EI 3 Sahulka HS Non-ground superposition
Superposition in practice
Slides
Slides (without animation)
Slides on Vampire proof visualisation
Recap/Exercises Thursday, May 23, 10:00-10:45 EI 3 Sahulka HS

Course Schedule and Organization

Lectures:

The course will be held semi-blocked, that is two lectures a week, in the period of March 7 - May 14, 2019, as follows:

Please consult the course calendar for further possible changes!

Exam:

The exam dates are as follows:

Please do not show up for both exam dates above!

For the exam, you are allowed to bring one A4-size paper of hand-written notes to the exam (both sides of the paper can be used). No other material is allowed.

Further exam dates, if needed, will be decided later, on individual requests.

Homeworks and Exercises:

There will be 3 homeworks, handed out online.
Corrected homeworks will be returned to students and discussed upon request in the regular course slot.

Number Problem Set Handed out on Due on Sample solutions
1 Homework 1 March 21, 2019 April 2, 2019 Sample solutions 1
2 Homework 2 April 15, 2019 May 2, 2019 Sample solutions 2
3 Homework 3 May 10, 2019 May 23, 2019 Sample solutions 3

Tools, binaries

The third block of the course on first-ordet theorem proving will be accompanied by the use of the Vampire theorem prover.
The binaries of Vampire can be compiled from https://vprover.github.io/download.html.

Course Information

Summary:

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.

Prerequisites:

The course is recommended for master and PhD students in Computer Science.

Lecture notes:

Lecture notes, that is slides, will be distributed online, at the end of each lecture.

Textbooks:

Many notions presented in the course are based on recent developments in automated deduction. As such, the course content does not follow any available textbook.
The best material to follow the course is the set of course sides.
For the SMT part of the course, a recommended additional textbook is "The Calculus of Computation" by A. Bradley and Z. Manna.

Grading and Examination:

Your course grade will be based on your homework and final exam scores.

Homeworks will count for 40% of the course grade. The final exam will count for 60% of the course grade.

The date and place of the final written exam will be announced later. You will be allowed to bring one A4-size sheet of hand-written notes to the exam. No other material is allowed.

Course Topics:

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.