**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 anonimized version.

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.

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 |

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

- Tuesdays, 10:15-11:45, EI 8 Poetzl HS;
- Thursdays, 9:15-10:45, EI 3 Sahulka HS.

The **exam dates** are as follows:

**Tuesday, June 11, 2019, 9:00-12:00, EI 8 Poetzl HS****Wednesday, June 12, 2019, 9:00-12:00, EI 10 Fritz Paschke HS**

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.

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 |

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.

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 is recommended for master and PhD students in Computer Science.

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.

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.

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 (SMT);
- satisfiability checking in combination of theories (SMT);
- validity proving in full first-order logic (superposition theorem proving).