COURSE AIMS AND OBJECTIVES: Insight into some aspects of mathematical logic contributing directly to current software technology.
COURSE DESCRIPTION AND SYLLABUS:
1. Proving in propositional and predicate calculi. Resolution and decision diagrams for the propositional calculus. Resolution for the predicate calculus. Herbrand's theorem. SLDresolution and logic programming, Prolog. Validity tests (semantic tableaux).
2. Temporal logic and model checking. Temporal formulae and their semantics. Kripke models and transition systems. Fairness, safety and liveness in distributed systems. Validity tests for LTL. Expressivity of LTL. Other models of time: CTL, CTL*. Model checking algorithms for LTL and CTL*. State abstraction and symbolic model checking. Model checking in software development  algorithms and tools.
3. Other modal logics in computer science. The logics of actions and programs, dynamic logic. Hoare's triples and program verification. The logics of knowledge and belief. Distributed and common knowledge. Modelling and verification with KT45n.
TEACHING AND ASSESSMENT METHODS:
Students' obligations during classes: Lecture and tutorial attendance, elaboration of homework, passing 2 midterm exams.
Signature requirements: Attendance at 70% of lectures and tutorials, submission of results for 70% of homework, passing grade at all midterm exams.
Taking of exams: Final examination is taken either in written or oral form. Final grade is based on successful elaboration of homework, grades for midterm exams and final examination grade.
