Automated Deduction (TU Wien, WS 2017/2018)

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 ten questions in this form and return it to us in an anonimized 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 8, 10:15-11:45 Seminarraum 354 Introduction
Course outlines
Slides (with animation)
Slides (no animation)
Lecture 2 Tuesday, March 13, 10:15-11:45 Seminarraum 125 Splitting
Conjunctive normal forms
Slides (with animation)
Slides (no animation)
Lecture 3 Thursday, March 15, 10:15-11:45 Seminarraum 354 Clausal normal forms
DPLL
Using a SAT solver
Slides (with animation)
Slides (no animation)
Lecture 4 Tuesday, March 20, 10:15-11:45 Seminarraum 125 Satisfiability and randomization
Satisfiability of Horn clauses
Slides (with animation)
Slides (no animation)
Lecture 5 Thursday, March 22, 10:15-11:45 Seminarraum 354 First-order logic and theories
Satisfiabilty modulo theories (SMT)
Theory of equality
Slides (with animation)
Slides (no animation)
Lecture 6 Tuesday, April 10, 10:15-11:45 Seminarraum 125 Congruence closure
SMT and non-unit clauses
Theory of arrays
Slides (with animation)
Slides (no animation)
Lecture 7 Thursday, April 12, 10:15-11:45 Seminarraum 354 SMT in combination of theories
Running an SMT solver
First-order theorem proving - an example
Slides (with animation)
Slides (no animation)
Lecture 8 Tuesday, April 17, 10:15-11:45 Seminarraum 125 First-order logic and TPTP
Inference Systems
Selection functions
Slides (with animation)
Slides (no animation)
Lecture 9 Thursday, April 19, 10:15-11:45 Seminarraum 354 Saturation algorithms
Redundancy elimination
Slides (with animation)
Slides (no animation)
Lecture 10 Tuesday, April 24, 10:15-11:45 EI 10 Paschke HS Guest lecture by Nikolaj Bjorner, Microsoft Research:
"Recent Trends in SMT and Z3"
Slides
Lecture 11 Thursday, April 26, 10:15-11:45 Seminarraum 354 Completeness of redundancy - guest lecture by Andrei Voronkov Slides
Lecture 12 Thursday, May 3, 10:15-11:45 Seminarraum 354 Equality
Ground superposition
Slides (with animation)
Slides (no animation)
Lecture 13 Tuesday, May 8, 10:15-11:45 Seminarraum 125 Unification and lifting
Non-ground superposition
Superposition in practice
Concluding remarks
Slides (with animation)
Slides (no animation)

Course Schedule and Organization

Lectures:

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

Please consult the course calendar for further possible changes!

Exam:

There are two slots for the final written exam, as follows:

You are allowed to bring one A4-size sheet of hand-written notes to the exam. No other material is allowed.

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 22, 2018 April 10, 2018 Sample solutions 1
2 Homework 2 April 19, 2018 May 3, 2018
3 Homework 3 May 8, 2018 May 21, 2018

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