Modal and Temporal Logic

Lecturer s : Ian Hodkinson (homepage) , Dirk Pattinson (homepage)
For course notes click on the lecturers homepages.

AIMS

To develop skills in the use of modal and temporal logics for specification, knowledge representation and practical reasoning in artificial intelligence and software engineering.

LEARNING OUTCOMES

Knowledge and understanding
Students should have assimilated the distinctive characteristics of modalities.

They should understand and recall the definitions of the logics and logical systems presented in the course, and the ideas of the proofs.

They should appreciate the differences in the logics, and their capabilities and limitations.

Skills and other attributes
a) intellectual skills - Students should be able to undertake simple proofs and examples, and modify coursework proofs appropriately to new situations. They should be able to follow the applications of modal logic in the computer science and AI literature.

b) practical skills - Students should gain familiarity with the issues involved in the use of modal and temporal logics in practical situations.

They should be able to recall relevant logics and reasoning techniques and modify and apply them accurately in appropriate situations.

c) transferable/key skills As above.

SYLLABUS Elements of propositional modal logics: syntax, Kripke frames and models, validity, frame correspondents of modal formulas, Sahlqvist's correspondence theorem. p-morphisms and bisimulations.
Temporal logic: various connectives. Advanced topics such as separation, interval temporal logic, hybrid logic, as time permits.

Systems of modal logic: deducibility, soundness, completeness, consistency. Completeness via canonical models, for K and other logics.

Filtration, finite model property, decidability.

Advanced topics such as modal mu-calculus, as tine permits.

PREREQUISITES

familiarity with propositional logic and acquaintance with classical first-order predicate logic - eg the contents of course 140.

COREQUISITES

none

POSTREQUISITES

none