Knowledge Representation and Reasoning

Assessment

100% by written examination.
Previous exam papers: 2004, 2005, 2006, 2007, 2008, 2009, 2010, 2011.

Reading

Reading material include the lecture notes, the textbook:
M. Huth nad M. Ryan, Logic in Computer Science, 2nd edition, Cambridge University Press, 2004, ISBN 0 521 54310 X
and selected papers on description logic: Introduction to DL, and Basic DL.

Additional recommended reading include
On epistemic logic:
R. Fagin, J.Y. Halpern, Y. Moses, M.Y. Vardi, Reasoning about Knowledge, MIT Press, 1995.
On modal/temporal logic:
R. Goldblatt, Logics of Time and Computation, CSLI, 1987 (1st edn.) and 1992 (2nd edn.). Available as pdf from here.

Module Outline

Propositional, modal, epistemic, temporal and description logic and their application in computer science.

Aims

In this module we will concentrate on logics that are applied in various branches of computer science, including distributed systems (reasoning about knowledge), artificial intelligence (knowledge representation) and software engineering (specification and verification). After a gentle introduction to the basics of propositional, modal and temporal logics (with an emphasis on semantics) students will learn how logic can be used as a formal tool in computer science: applications range from multi-agent systems and the world wide web to code verification.

Syllabus

Logical formalisms: basic properties (syntax and semantics) and concepts (truth, consequence) of:

• Propositional logic
• Modal and epistemic logic
• Temporal logic
• Description logic

Applications (the following list contains some application areas that we may look at during the module depending on students' interests)

• Reasoning about knowledge: modelling knowledge in multi-agent systems (including common and distributed knowledge, agreement), describing the behaviour of a system by using the knowledge of the participating agents

• Programme verification: transition systems and computations, verification of concurrent programs

• Knowledge representation: knowledge bases, reasoning about knowledge (consistency checking, deriving knowledge)

Lectures

• Week 1.
  Motivation - the use of logic in computer science. Modelling distributed systems using epistemic logic, knowledge representation using description logics, program verification using temporal logic.
  Mathematical Background (Naive Set Theory and Induction) notes. Sets, operations on sets (union, intersection, complement, direct product, power set), cardinality (when two sets have the same number of elements).
• Week 2.
  Mathematical Background (ctd.). Relations as products of sets, mathematical and structural induction (a powerful proof method by establishing a base case and then showing "inheritance").
• Week 3.
  Propositional Logic notes. Syntax: logical connectives (conjunction, disjunction, negation, implication) and well-formed formulas, parse tree, subformulas. Semantics: meaning/truth values of formulas, valuations, truth tables, satisfiability, validity, logical consequence. Formalizing arguments.
• Week 4.
  More Propositional Logic. Semantic tableaux: a formal method for establishing satisfiability of formulas. Decidability: general procedures for determining which are the valid/satisfiable formulas.
• Week 5.
  Basics of Modal Logic (motivation, syntax and semantics, satisfiability and validity): different modes of truth (depending on time, location, belief, knowledge, etc.), modalities (boxes and diamonds), meanings of formulas by possible world semantics. notes.
  See Jan Jaspars' animations for logic.
• More on Modal Logic: various flavours of ML (frame conditions), decidability (mosaic method as a general procedure for determining which are the true formulas), model checking (determining whether a formula is true in a given model).
• Basics of Epistemic Logic: modelling knowledge in multi-agent systems, common and distributed knowledge, the muddy children puzzle.
• Temporal Logic: flows of time, temporal connectives (future, past, next time).
  Temporal Epistemic Logic: the hangman (unexpected exam) paradox.
• Models of Computations: programs and transition systems, invariance properties, assertion strengthening, assertion propagation.
• Basics of Description Logic: T- and A-boxes, knowledge bases, consistency checking, subsumption, deriving knowledge.