COMP20141: Logic and Modelling (2009-2010)
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.
A student completing this course unit should:
Have a knowledge about basic reasoning (or satisfiability-checking) algorithms for propositional logic (A).
Have a knowledge of quantified boolean formulas and basic understanding of bound variables and quantifiers (A).
To understand BDDS (binary decision diagrams) as a data structure for compact representation of propositional formulas (A).
Have a knowledge about applications of propositional logic (such as finite domain constraint satisfaction and planning) and be able to apply it for solving hard combinatorial problems (B and C).
Have a knowledge of simple temporal logics (A).
Be able to formally specify finite-state concurrent systems as transition systems (B)
Be able to specify properties of simple transition systems in temporal logics (B).
Assessment of Learning outcomesAll learning outcomes are assessed both by both examination and exercises.
Contribution to Programme Learning OutcomesA1, A2, A5, B1, C5 and C6.
Available on the course Web page.
The reading material is a collection of notes available on the course Web page. In addition, slides used during lectures are available on the course Web page as well.