Skip to navigation | Skip to main content | Skip to footer

Current postgraduate taught students

COMP61132: Modal Logic and Description Logics (2010-2011)

This is an archived syllabus from 2010-2011

Modal Logic and Description Logics
Level: 6
Credit rating: 15
Pre-requisites: Logic and Applications, or familiarity with propositional and first-order (predicate) logic
Co-requisites: none
Duration: 6 weeks long; teaching will take place on 1 day per week for 5 weeks
Lectures: Lecturers will be interspersed with examples classes and labs
Examples classes: Examples classes will take place on teaching days
Labs: Labs will take place on teaching days
Lecturers: Uli Sattler, Renate Schmidt
Course lecturers: Uli Sattler

Renate Schmidt

Additional staff: view all staff
Sem 2 P4 Lecture 2.19 Thu 09:00 - 17:00 -
Assessment Breakdown
Exam: 50%
Coursework: 50%
Lab: 0%

Themes to which this unit belongs
  • Semantic Technology


For many applications, specific domain knowledge is required. Instead of coding such knowledge into a system in a way that it can never be changed (hidden in the overall implementation), more flexible ways of representing knowledge and reasoning about it have been developed in the last 10 years. These approaches are based on various extensions of classical logic: modal logic, agents logics, or description logics. These logics can be used to reason about the terminology of a domain or the behaviour of systems. Computer-based tools can then use this kind of reasoning to support the user. In particular, modal logics provide the foundations for multi-agent systems and description logics are being used as foundational tools for the semantic web and ontology reasoning.


This course unit provides an introduction to various extensions of classical logic, how to formalise knowledge and questions about this knowledge in these logics and how to use automated reasoning techniques for answering these questions. The course unit aims to:
provide students with an understanding of different kinds of knowledge and the logics developed to represent this kind of knowledge together with the underlying theory necessary for applying automated reasoning systems (based on modal and description logic)
study a range of techniques to formalise and represent knowledge within these logics, and,
finally, allow students to use various automated reasoning tools to reason about knowledge represented in these logics.

Programme outcomeUnit learning outcomesAssessment
G1Have knowledge and understanding of the syntax and semantics of various modal and description logics.
  • Examination
  • Individual coursework
G1Have knowledge and understanding of important notions such as soundness, completeness, decidability, undecidability.
  • Individual coursework
  • Examination
G1 G2Be able to formalise and represent knowledge in these logics and relate questions concerning this knowledge to logical reasoning problems.
  • Examination
  • Individual coursework
G1 G2Have knowledge and understanding of a selection of logic-based applications.
  • Examination
  • Individual coursework
G2Be able to use reasoning approaches, in particular, tableau and justification computation for description logic, and tableau, model checking and computing correspondence properties for modal logics.
  • Individual coursework
G1Have knowledge and understanding of implementation aspects of reasoning systems.
  • Individual coursework
G3Be able to use various systems and apply them to solve problems.
  • Individual coursework
G4Study in more detail one topic related to the course, undertaking a literature search and producing a summary essay.
  • Individual coursework


The following lists topics to be covered in course. The number of lectures for each topic are given in brackets.

1. Introduction to Modal and Description Logic (1 lecture):

2. Description Logics (5 lectures):

Lanaguage and meaning of ALC: syntax, semantics, satisfiability of concepts;
Reasoning using a simple tableau calculus for concept satisfiability (which is terminating, with proof sketch of soundness, completeness & termination));
Storing information in TBoxes and Aboxes, models, consistency;
Extend tableau calculus to decide consistency of TBoxes and ABoxes;
Discuss other reasoning problems (concept subsumption, concept satisfiability wrt TBoxes) and how to reduce to consistency;
Relationship to first-order logic;

3. Justifications and Explanations for Description Logic Entailment (2 lectures):

Definitions and examples;
Using justifications within P4 or kudu, brief relation between description logics and OWL, Manchester syntax;
How justifications can be computed;

4. Decidability and Undecidability (3 lectures):

Non-termination of tableau reasoning for consistency of TBoxes and ABoxes, achieving termination with blocking;
Extend ALC with general role value maps (as global axioms) and prove undecidability;
Extend ALC with transitivity (as special case of global role value maps) and inverse roles;
Extend tableau calculus and blocking, sketch proof that it is still sound, complete, and terminating;

5. Modal Logics (7 lectures):

Syntax, semantics of multi-modal logic K and tense logic with nominals, different readings of modal operators, relationship to description logic and first-order logic;
Model checking;
Satisfiability, validitity in frames, modelling agents;
Correspondence property, modal expressivity, agent logics;
Computing correspondence properties;
Tableau calculi for modal logics;
Modal logic of some, all and only, plus tableau with unrestricted blocking;

6. Implementing tableau calculi (2 lectures):

Handling non-determinism in reasoning calculi, techniques to reduce branching and duplicate search;
Clever backtracking and backjumping;

7. Things left out (1 lecture):

Other expressive means/logical constructors, other reasoning techniques, other reasoning problems, other implementation issues;


Exercises and assignments are of varying difficulty. Some exercises and assignments are to be done with pencil and paper, some will require the use of tools.

Additional Information

Additional information may be found at the course unit webpage.

Reading List

The following gives a selection of books that would be useful to refer to. There are many other textbooks available on the topics covered. Further references may be given during lectures.

Notes will made available to cover the systems and all of the various topics presented in the course.

Supplementary Text
Title: Description logic handbook: theory, implementation and applications (chapter by Baader, Franz & Werner Nutt: "Basic description logistics", pp. 43 - 95)
Author: Baader, Franz et al (eds.).
ISBN: 0521781760
Publisher: Cambridge University Press
Year: 2003

Supplementary Text
Title: Logic in Computer Science: modelling and reasoning about systems (2nd edition)
Author: Huth, Michael and Mark Ryan
ISBN: 9780521543101
Publisher: Cambridge University Press
Edition: 2nd
Year: 2004