After successful completion of the course, students are able to explain and apply algorithmic techniques and fundamental results in automated deduction, such as SAT/SMT solving and superposition reasoning.

Due to the recent drastical developments in the COVID-19 coronavirus, all lectures between March 11 - (at least) April 16 will be held online. Lecture recordings and slides will be posted online on the TUWEL site of the course, with course-related discussions monitored online.

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

There will be two lectures a week, with lecture slides online accompanying the lectures. 

Exercises will be discussed during the lecture, and homeworks will be made online.

Due to the recent drastical developments in the COVID-19 coronavirus, lecture recordings and slides will be posted online on the TUWEL site of the course. 

There will be 5 homeworks, handed out online. 

Corrected homeworks will be returned to students and discussed upon request in the regular course slot.  Homework solutions will also be discussed during regular lecture time.

There will be two recap sessions: mid-term and end of course.

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

The first lecture is on March 5 9:15--10:45, in EI 3 Sahulka HS.

Due to the recent drastical developments in the COVID-19 coronavirus, lecture recordings and slides will be posted online on the TUWEL site of the course. 

The course grade will be based on five written homework assignments and a written exam.

Homework assignments count for 40% of the course grade.

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

For slides and other material see the TUWEL course.