Current postgraduate taught students
COMP60162: Knowledge Representation and Reasoning (2007-2008)
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. They 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 description logics have recently been used as foundational tools for the semantic web.
This course unit aims to provide 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 systems for answering these questions. Students should have some knowledge about logic and will deepen it in the first pre-course week. 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 propositional, first order, 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.
A student completing this course unit should:
have knowledge and understanding of the syntax and semantics of modal, description, and temporalised description logics, defaults, and formal concept analysis (A)
1. be able to formalise and represent knowledge in these logics and relate questions concerning this knowledge to logical reasoning problems (A and B)
2. have knowledge and understanding of a selection of logic-based applications (A and B)
3. be able to use standard proof systems, in particular Hilbert-style deduction and a translation-based approach for modal logics, subsumption algorithms for description logics (B)
4. be able to use various systems (SPASS, ICOM) and apply them to solve problems (C)
Assessment of Learning outcomesLearning outcomes (1), (2), (3), (4) will be assessed by exam. All learning outcomes will be assessed via coursework exercises.
Contribution to Programme Learning OutcomesA1, A2, B2, B3, and C3
The following lists topics to be covered in the pre-course work and taught week. The number of lectures for each topic are given in brackets. If the topic is to be covered in the pre-course work or in the supervised labs, then this is also indicated:
Introduction and motivation.
Including example problems, problem representation via logic, computer assisted reasoning in mathematics.
Elementary set theory.
What is a set, a relation, a function, set operations (intersection, union, etc), properties of binary relations (reflexivity, symmetry, transitivity, etc).
Theory, language, models, validity and satisfiability, inference rules, soundness and completeness, reasoning methods: truth tables, proof by contradiction.
First order logic formulae, their meaning, validity and satisfiability, translating between natural language and first-order logic.
Early knowledge representation formalisms .
Nonmonotonic inheritance networks, frame-based systems.
First-Order Logic [2, supervised lab].
First order logic formulae, their meaning, reasoning problems, useful normal forms, inference calculus, undecidability and semi-decidability.
Modal Logic: Representation and reasoning on the semantical level [4.5, supervised lab].Modal logic, possible worlds semantics, model checking, satisfiability and validity, correspondence theory.
Modal Logic: Reasoning calculi, agent applications [4, supervised labs].
Logically omniscience problem, belief logic, epistemic logic, deduction in Hilbert systems, deduction via translation to first-order logic.
Description logics [3.5, supervised labs].
Language of description logics, meaning of description logic statements, reasoning calculi, introduction to the semantic web and ontologies using description logics.
Icom [2, supervised labs].
EER diagrams, relationship between EER diagram and description logic, reasoning about EER diagrams.
Non-standard reasoning services in description logics [2, supervised labs].
Least common subsumers, most specific concepts, and their usage in description logic applications.
Temporal logic [3, supervised labs].
The temporal logic LTL, its extension to temporalised modal and description logics, their applications.
Defaults, in propositional and first order logic [3, supervised labs].
Defaults, motivation for ordered defaults, e.g. in description logics, their applications.
Exercises and assignments are of varying difficulty - those in the teaching week are aimed to consolidate the material of the lectures and are thus easier. Some exercises and assignments are to be done with pencil and paper, some will require the use of tools (SPASS for the ML, ICOM for the DL part).
Additional information may be found at the course unit webpage
There is no single book covering all the material, but the following gives a good introduction to logical systems and reasoning methods:
Notes will made available to cover the systems (SPASS and ICOM) and all of the various topics presented in the course.
There are many other textbooks available on the topics covered. The following gives a selection of those that would be useful to refer to:
Recommended reading is Chapter 3 on modal logic and its applications in the book by M. Huth and M. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, 2000.
Recommended Reading is the chapter by F. Baader and W. Nutt, Basic Description Logics, in the Description Logic Handbook (edited by F. Baader, D. Calvanese, D.L. McGuinness, D. Nardi, P.F. Patel-Schneider, Cambridge University Press, 2002, pp. 47-100).
Further details will be presented in the taught week.
Supplementary TextTitle: Description Logic Handbook
Author: Franz Baader, Diego Calvanese, Deborah Mcguinness, Daniele Nardi, Peter Patel-Schneider
Publisher: Cambridge University Press
Supplementary TextTitle: Logic in Computer Science: modelling and reasoning about systems (2nd edition)
Author: Michael Huth, Mark Ryan
Publisher: Cambridge University Press
Supplementary TextTitle: Essence of logic
Author: Kelly, John
Publisher: Pearson Education Limited