Current postgraduate taught students
COMP61132: Modal Logic and Description Logics (2010-2011)
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 outcome||Unit learning outcomes||Assessment|
|G1||Have knowledge and understanding of the syntax and semantics of various modal and description logics.|
|G1||Have knowledge and understanding of important notions such as soundness, completeness, decidability, undecidability.|
|G1 G2||Be able to formalise and represent knowledge in these logics and relate questions concerning this knowledge to logical reasoning problems.|
|G1 G2||Have knowledge and understanding of a selection of logic-based applications.|
|G2||Be 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.|
|G1||Have knowledge and understanding of implementation aspects of reasoning systems.|
|G3||Be able to use various systems and apply them to solve problems.|
|G4||Study in more detail one topic related to the course, undertaking a literature search and producing a summary essay.|
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;
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;
CourseworkExercises 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 InformationAdditional information may be found at the course unit webpage.
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 TextTitle: 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.).
Publisher: Cambridge University Press
Supplementary TextTitle: Logic in Computer Science: modelling and reasoning about systems (2nd edition)
Author: Huth, Michael and Mark Ryan
Publisher: Cambridge University Press