Reasoning about Information Update:  2011-2012

Overview

The course is addressed to both MSc students (in Mathematics, CS and MFoCS) and third year undergarduate students (in any of the following fields: Maths, CS, Maths and Comp, MMath, and Maths and Philosophy), with an interest in Logic, AI and the dynamics of information in multi-agent systems. It explores and compares various logical approaches to information flows based on the use of modal logics, on formal languages for the specification of knowledge-related features of a system, and on the use of sequent calculi and proof theory as well as their order theoretic algebraic semantics, as abstract models for information update. A range of important mathematical techniques, such as soundness, completeness, building proof trees, using algebraic axioms via rewriitng,  and concepts, such as uncertainty, belief, knowledge, update,  are introduced and explained. The course presents applications of these notions to the analysis of information update, communication, and navigation, and of the role of beliefs and belief-changing actions, in the overall dynamics of any "society" of intelligent agents. In particular, we will model and reason about  epistemic puzzles,  robot navigation protocols, verification of protocols of unmanned vehicles,  communication between unreliable or adversary agents over insecure channels. Implementation of these applications are studied by presenting rule based systems based on the sequent calculus and rewrite systems based on the algebra.

Learning outcomes

At the end of the course students are expected to:

• Analyze and model interactive scenarios of multi-agent information systems and reason about them using the formal logics
• Learn syntax, proof systems and algebraic semantics for modal logics of actions and propostions
• Become able to reason about epistemic attitudes such as uncertainty, belief, knowledge and their update as a result of communication and navigation
• Derive dynamic properties of information, using the presented proof system and by drawing proof trees.
• Prove the above properties using the algebraic axiomatics in the form of rewrite rules
• Implement the proof rules and algebraic axioms using rule-based programming languages such as Prolog and Haskel
• Become familar with epistemic puzzles, navigation protcols, and protocols of unmanned vehicles, used as test cases of the course

Synopsis

Week 1. Examples of multi-agent systems and scenarios: NASA Deep Space shuttle, air traffic control,  eBay, Amazon, epistemic puzzles, security protocols, UAV protocols, robot navigation protocols

Week 2. Syntax and proof theory for a modal logic of actions, examples from puzzles and protocols

Week 3. Synax and proof theory for a modal logic of propositions, examples from puzzles and protocols

Week 4. Assumption Rules

Week 5. Modeling the muddy children puzzle and solving it

Week 6. Algebraic semantics for the modal logic of actions

Weeks 7. Algebraic semantics for the modal logic of propositions

Week 8. Modelling a robot navigation protocol and proving its properties

Reading list

Introductory Reading: Modal logics of propostions and actions

• Chapters 1,2,3 of: R. Fagin, J, Halpern, Y. Moses, M. Vardi. Reasoning about Knowledge, MIT Press, 1995.
• Chapter 5 of D. Harel, D. Kozen, J. Tiuryn. Dynamic Logic, The MIT Press, 2000.
• Cahpters 1 to 5 of P. Blackburn, M. de Rijke, Y. Venema. Modal logic, Cambridge University Press, 2001.

Sequent Calculi for modal logics of actions and propositions

• to be updated

Algebraic Semantics for modal logics of actions and propositions

• to be updated

Further Reading: Multi-Agent Systems

• M. Wooldridge. An Introduction to Multi-agent Systems, John Wiley & Sons, 2002. (slides of a course based on this book are available from http://www.csc.liv.ac.uk/~mjw/pubs/imas/distrib/)

Feedback

Students are formally asked for feedback at the end of the course. Students can also submit feedback at any point here. Feedback received here will go to the Head of Academic Administration, and will be dealt with confidentially when being passed on further. All feedback is welcome.

Taking our courses

This form is not to be used by students studying for a degree in the Department of Computer Science, or for Visiting Students who are registered for Computer Science courses

Other matriculated University of Oxford students who are interested in taking this, or other, courses in the Department of Computer Science, must complete this online form by 17.00 on Friday of 0th week of term in which the course is taught. Late requests, and requests sent by email, will not be considered. All requests must be approved by the relevant Computer Science departmental committee and can only be submitted using this form.