After successful completion of the course, students are able to
- model problems rigorously using logic
- reason and prove problems algorithmically
- solve problems by means of computer-assisted tools.
Logic offers precision and trust and it is at the base of very many applications in various fields. Logic-based automated reasoning is undergoing a rapid development thanks to its successful use in Artificial Intelligence, system development, software verification, security analysis, theorem proving in mathematics, legal reasoning and many other areas.
This course focuses on modeling, proving and solving computer science challenges using automated reasoning techniques in various fragments of first-order logic. In particular, we will focus on specialised algorithms for modeling and solving problems in propositional logic, and combination of data stucture theories.
We will address both the theoretical and practical aspects of logical formalization, developing reasoning procedures, and using computer-supported methods for solving computer science challenges.
The tentative list of topics covered by the course is below:
- mathematical foundations
- propositional and first-order logic: syntax, semantics and formalizations
- satisfiability checking in propositional logic (splitting, DPLL);
- proof calculi
- satisfiability checking in the theory of arithmetic, uninterpreted functions and arrays;
- satisfiability checking with respect to some background theory (Satisfiability Modulo Theories SMT);
- hands-on sessions using SAT solvers, SMT solvers and first-order theorem provers.
The topics of the course are presented during in-class lectures. Lecture slides accompanying the lectures will be made online. Lectures will be recorderd and recordings will also be made online.
Short quizzes will be made online and should be completed. These quizzes will assess the general understanding of the lecture topics. There will be all together 6 quizzes, with each quiz leading to a maximum of 10 points.
Exercise sessions are included within regular lectures, allowing students to consolidate and practice their knowledge. There will be three blocks of homeworks, with each block coming with a new exercise sheet. Per exercise sheet, students will have to solve 2 exercise problems and 1 tool-based reasoning task.
In order to enter the written exam, students are required to
- have gained at leat 40 points from the 6 online quizzes;
- have completed 3 exercises per exercise sheets, submitted in due time.
The exam is a regulated open-book, written exam. Regulated open-book means that students are allowed to bring printed lecture notes (in whatever paper format), but they are not allowed to use of any electronic device during the exam.
