MMath Mathematics and Statistics

The course is focused on logic, reasoning algorithms and formal methods. 
In the course we cover several logics widely used in applications ranging from verification of software and hardware to mathematical reasoning. The course will cover formal aspects of propositional logic, quantified propositional logic (QBF), linear temporal logic. We study major reasoning algorithms for these logics including DPLL, tableaux, randomized algorithms, OBDDs. The course also covers formalization of problems such as state transition systems and specification and verification of properties of such systems using logic. 

COMP11120 (for CS students) and MATH11121 or equivalent (for CM students).

COMP11120 (for CS students) and MATH11121 or equivalent (for CM students).

This course intends to build an understanding of fundamentals of (mathematical) logic as well as some of the applications of logic in modern computer science, including hardware verification, finite domain constraint satisfaction and verification of concurrent systems. 

ILO 1: Understand linear temporal logic (LTL), syntax, semantics and be able to evaluate LTL formulas on computation paths, check equivalence of  LTL formulas.

ILO 2: Understand model checking algorithms and be able to apply model checking algorithms to  verification of state transition systems.

ILO 3: Encode problems from different domains into propositional logic (such as finite domain constraint satisfaction).

ILO 4: Understand OBDDs (ordered binary decision diagrams) as a data structure for compact representation of propositional formulas and be able to construct and combine OBDDs.

ILO 5: Understand propositional logic and be able to apply satisfiability-checking algorithms to solve problems in propositional logic.

ILO 6: Understand quantified Boolean logic and be able to apply reasoning algorithms to evaluate formulas in quantified Boolean logic.

ILO 7: Formally specify finite-state transition systems as transition graphs and using symbolic representation.

The course is focused on logic, reasoning algorithms and formal methods. 
In the course we cover several logics widely used in applications ranging from verification of software and hardware to mathematical reasoning. The course will cover formal aspects of propositional logic, quantified propositional logic (QBF), linear temporal logic. We study major reasoning algorithms for these logics including DPLL, tableaux, randomized algorithms, OBDDs. The course also covers formalization of problems such as state transition systems and specification and verification of properties of such systems using logic. 

Lectures

22 in total, 2 per week, including some feedback sessions on exercises

My Website of this course will contain a lot of material, including solutions to exercises