50009

Symbolic Reasoning

Module aims

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 artificial intelligence. It also provides the theoretical background for more advanced modules in these areas.

Learning outcomes

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

Module syllabus

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

Teaching methods

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.

An online service will be used as a discussion forum for the module. 

Assessments

There will be two assessed coursework that, combined, contribute 20% of the mark for the module. There will be a final written exam, which counts for the remaining 80% 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 leaders

Mr Charles Pert
Dr Dalal Alrajeh