This course for senior (fourth year) or graduate students is an introduction to the syntax and semantics of modal logic. It is also a NICTA co-listed graduate course. Modal logic is useful in many application areas in CS such as artificial intelligence, computer security, correctness of network protocols, agent technology, and language understanding. However, the course will only provide the common core needed for these applications without going into specifics.
It begins with motivations for modality, a quick tour of Kripke structures and typical axioms like K, T, 4 and 5, especially in the settings pertinent to computer science, e.g., in AI, programming languages, and temporal reasoning. Then in a second pass rigorous versions of the intuitive notions are introduced, proceeding to soundess and completeness via the canonical model theorem. Filtrations are introduced, and questions of decidabilty and complexity are discussed. Applications to logics of programs, belief and knowledge are then considered. If time permits, first-order modal logic is briefly examined.
An acquaintance with propositional logic (or its equivalent in switching logic in EE) is assumed, and the ability to do mathematical proofs involving induction, contradiction, etc., which feature in standard discrete mathematics courses at the second year (sophomore) level. Distinction-level junior (third year) students may also enroll with the permission of the instructor. Mail the course instructor Norman Foo (norman at cse.unsw.edu.au) for permission to enroll.
This year (S2, 2004) the course will be run as a guided reading course, with lectures being a tour of the text. The content will be stipulated by sections of the text that you have to read, and assignments you have to hand in. I will follow the text closely, and use transparencies of pages in it for the lecture commentary, but also write on the board when I have to explain technicalities. You may have to make presentations to us all from time to time about the material you read.
During the periods that I am out of town or busy, someone else (a faculty member, a postdoctoral fellow, or a NICTA scientist) will take my place.
Class meetings are 2-5pm Wed in EE222. This is also in the time-table on the School home page.