This module covers the foundations of symbolic reasoning: SAT solving, logic programming, answer set programming, and SMT solving. It equips you with the practical skills necessary to use to solve real-world problems in program reasoning and symbolic articial intelligence. It also provides the theoretical background for more advanced modules in these areas.
Upon successful completion of this module you will be able to:
- describe theoretical foundations of Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solving
- implement algorithms for SAT solving
- encode problems in SMT form and solve them using state-of-the-art SMT solvers
- explain the theoretical foundations of logic programming
- apply resolution as an inference system for logic programming
- encode problems using Answer Set Programming (ASP) and solve them using state-of-the-art ASP solvers
The module is divided into four parts:
1.Boolean Satisfiability (SAT):
- The SAT problem and its NP-complete status
- The DP and DPLL algorithms for SAT solving
- The abstract DPLL framework and conflict-driven clause learning
2. Theoretical foundation of knowledge representation and reasoning in AI:
- Logic programming syntax
- Definite logic programs semantics: herbrand models, minimal models, immediate consequent operator
- Normal logic programs semantics: stratification, iterative fixed point, stable models, answer set semantics
3. Methods and approches for knowledge-driven inference:
- Inference systems: SLD resolution and SLDNF resolution
- Answer set programming: syntax, choice rules, aggregation, optimization statements, hard constraints and weak constraints
4. Satisfiability Modulo Theories (SMT)
- A variety of first-order theories and their decidability
- Lazy SMT solving
- The DPLL(T) architecture for SMT solving
The material will be taught through lectures, backed up by formative exercises designed to reinforce the material as it is taught. Approximately one third of the timetabled activities will be dedicated to problem solving, using selected formative exercises as examples. Some of these will be in the form of small-group laboratory exercises, in order to encourage group discussions and group problem solving. These exercises wil reinforce the practical aspect of the material through application to real-word problems.
The EdStem Q&A web service will be used as an open online discussion forum for the module.
There will be two assessed coursework that, combined, contribute 15% of the mark for the module. There will be a final written exam, which counts for the remaining 85% of the marks.
Detailed verbal feedback will be given on the exercises covered in the tutorial/lab sessions. Written feedback will be given on assessed work.
Module leadersDr Dalal Alrajeh
Professor Alastair Donaldson